Reference · Finite types, distributions and Markov chains

rainbow.math.finite.metric-separation

Finite types, distributions and Markov chainssrc/rainbow/math/finite/metric_separation.clj0 definitions, 6 theorems

Constructive zero and positivity separation for finite natural sup-distance.

nat/equal-zero-of-at-most-zero :
  (value : ℕ)
  (ordered : value ≤ 0)
  → value = 0

list/nat-map-max-zero-of-memberwise-zero.{u} :
  (A : Type u) (mapping : A → ℕ) (source : List A)
  (memberwise-zero : ∀ (value : A), ∀ (member : list/membership A source value), mapping value = 0)
  → list/nat-map-max A mapping source = 0

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

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

metric/finite-sup-zero-equivalent-pointwise-equal.{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-sup-distance A source left right

metric/finite-sup-positive-of-pointwise-not-equal.{u} :
  (A : Type u) (source : Finset A) (left right : A → ℕ) (state : A)
  (member : state ∈ source)
  (different : left state = right state → proposition/falsity)
  → nat/strict-below 0 (distance)
  where distance := metric/finite-sup-distance A source left right