Reference · Finite types, distributions and Markov chains

rainbow.math.finite.signed-sup-separation

Finite types, distributions and Markov chainssrc/rainbow/math/finite/signed_sup_separation.clj0 definitions, 3 theorems

Exact separation for finite signed-valued function sup distance. Pointwise signed equivalence on every enumerated member is equivalent to zero finite sup distance. The converse is intentionally scoped to the finset's members; a client claiming equality over an entire carrier must separately provide exhaustiveness. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.signed-sup-distance

metric/finite-signed-sup-distance-zero-of-pointwise-equivalent.{u} :
  (A : Type u) (source : Finset A) (left right : A → ℚ)
  (pointwise : ∀ (state : A), ∀ (member : state ∈ source), left state = right state)
  → metric/finite-signed-sup-distance A source left right = 0

metric/pointwise-equivalent-of-finite-signed-sup-distance-zero.{u} :
  (A : Type u) (source : Finset A) (left right : A → ℚ)
  (radius-zero : metric/finite-signed-sup-distance A source left right = 0)
  (state : A)
  (member : state ∈ source)
  → left state = right state

metric/finite-signed-sup-distance-zero-iff-pointwise-equivalent.{u} :
  (A : Type u) (source : Finset A) (left right : A → ℚ)
  → proposition/conjunction (distance = 0 → (∀ (state : A), ∀ (member : state ∈ source), left state = right state)) ((∀ (state : A), ∀ (member : state ∈ source), left state = right state) → distance = 0)
  where distance := metric/finite-signed-sup-distance A source left right