Reference · Finite types, distributions and Markov chains

rainbow.math.finite.nnrat-sup-distance

Finite types, distributions and Markov chainssrc/rainbow/math/finite/nnrat_sup_distance.clj1 definitions, 6 theorems

A native finite supremum metric for NNRAT-valued functions. Bellman values are functions into exact nonnegative rationals, while Rainbow's existing finite function metric is Nat-valued and its signed supremum metric is list-vector-specific. This module closes that representation gap without inventing quotient subtraction on NNRAT: each value is embedded canonically with `signed/from-nnrat`, scalar distance is the existing quotient-safe signed distance, and the finite maximum is the existing signed map-max fold over the exact finset enumeration. The result has the laws needed by a posteriori Bellman certificates: every enumerated component is below the supremum, pointwise bounds fold globally, and the metric is nonnegative, symmetric, and triangular. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.signed.vector-sup-triangle

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

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

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

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

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

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

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