Reference · Finite types, distributions and Markov chains

rainbow.math.finite.nnrat-sup-radius

Finite types, distributions and Markov chainssrc/rainbow/math/finite/nnrat_sup_radius.clj2 definitions, 6 theorems

A Bellman-compatible NNRAT supremum radius over exact finite carriers. Unlike the signed-valued metric view, this fold stays in NNRAT, so its result can be supplied directly as the epsilon parameter of Rainbow's finite Bellman contraction theorems. It maps each enumerated state to the exact `nnrat/distance` of the two values and folds with the decidable NNRAT maximum. The package proves the two directions a residual certificate needs: every member distance is below the finite radius, and any uniform pointwise bound bounds the radius. Nonnegativity is structural from the zero base. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.nnrat.distancemath.rational.nnrat.minmax

list/nnrat-map-max.{u} :
  (A : Type u) (mapping : A → ℚ≥0) (x₁ : List A)
  → ℚ≥0

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

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

list/nnrat-map-max-bounded.{u} :
  (A : Type u) (mapping : A → ℚ≥0) (upper : ℚ≥0)
  (zero-upper : 0 ≤ upper)
  (source : List A)
  (pointwise : ∀ (value : A), ∀ (member : list/membership A source value), mapping value ≤ upper)
  → list/nnrat-map-max A mapping source ≤ upper

list/nnrat-map-max-nonnegative.{u} :
  (A : Type u) (mapping : A → ℚ≥0) (source : List A)
  → 0 ≤ list/nnrat-map-max A mapping source

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

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

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