Reference · Finite types, distributions and Markov chains

rainbow.math.finite.metric

Finite types, distributions and Markov chainssrc/rainbow/math/finite/metric.clj3 definitions, 11 theorems

Constructive maximum folds and finite sup-distance over exact finite data.

nat/recursive-max :
  (x₁ x₂ : ℕ)
  → ℕ

list/nat-map-max.{u} :
  (A : Type u) (mapping : A → ℕ) (x₁ : List A)
  → ℕ

metric/finite-sup-distance.{u} :
  (A : Type u) (source : Finset A) (left right : A → ℕ)
  → ℕ

nat/recursive-max-left-bound :
  (left right : ℕ)
  → left ≤ nat/recursive-max left right

nat/recursive-max-right-bound :
  (left right : ℕ)
  → right ≤ nat/recursive-max left right

nat/recursive-max-commutative :
  (left right : ℕ)
  → nat/recursive-max left right = nat/recursive-max right left

nat/recursive-max-is-left-or-right :
  (left right : ℕ)
  → proposition/disjunction (nat/recursive-max left right = left) (nat/recursive-max left right = right)

nat/recursive-max-least-upper-bound :
  (left right upper : ℕ)
  (left-bound : left ≤ upper)
  (right-bound : right ≤ upper)
  → nat/recursive-max left right ≤ upper

list/nat-map-max-upper-bound.{u} :
  (A : Type u) (mapping : A → ℕ) (source : List A) (value : A)
  (member : list/membership A source value)
  → mapping value ≤ list/nat-map-max A mapping source

list/nat-map-max-bounded.{u} :
  (A : Type u) (mapping : A → ℕ) (upper : ℕ) (source : List A)
  (pointwise : ∀ (value : A), ∀ (member : list/membership A source value), mapping value ≤ upper)
  → list/nat-map-max A mapping source ≤ upper

list/nat-map-max-congruent.{u} :
  (A : Type u) (left right : A → ℕ)
  (pointwise : ∀ (value : A), left value = right value)
  (source : List A)
  → list/nat-map-max A left source = list/nat-map-max A right source

metric/finite-sup-upper-bound.{u} :
  (A : Type u) (source : Finset A) (left right : A → ℕ) (state : A)
  (member : state ∈ source)
  → nat/distance (left state) (right state) ≤ metric/finite-sup-distance A source left right

metric/finite-sup-symmetric.{u} :
  (A : Type u) (source : Finset A) (left right : A → ℕ)
  → metric/finite-sup-distance A source left right = metric/finite-sup-distance A source right left

metric/finite-sup-triangle.{u} :
  (A : Type u) (source : Finset A) (left middle right : A → ℕ)
  → metric/finite-sup-distance A source left right ≤ algebra/nat-add (distance₁) (distance)
  where distance := metric/finite-sup-distance A source middle right
  where distance₁ := metric/finite-sup-distance A source left middle