Reference · Finite types, distributions and Markov chains

rainbow.math.finite.signed-sup-distance

Finite types, distributions and Markov chainssrc/rainbow/math/finite/signed_sup_distance.clj1 definitions, 5 theorems

A native finite supremum metric for signed-valued functions. `metric/finite-signed-sup-distance` folds quotient-safe signed distance over an exact finset enumeration with the established signed maximum. This is the function-space counterpart of `vector/sup-distance`, and supplies the metric laws needed by residual certificates for finite signed Bellman operators. The carrier enumeration need not be exhaustive for the fold laws themselves; clients that turn them into carrier-wide claims must retain an explicit coverage premise. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.nnrat-sup-distance

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

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

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

metric/finite-signed-sup-distance-nonnegative.{u} :
  (A : Type u) (source : Finset A) (left right : A → ℚ)
  → 0 ≤ metric/finite-signed-sup-distance A source left right

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

metric/finite-signed-sup-distance-triangle.{u} :
  (A : Type u) (source : Finset A) (left middle right : A → ℚ)
  → distance right ≤ distance middle + metric/finite-signed-sup-distance A source middle right
  where distance := metric/finite-signed-sup-distance A source left