Reference · Finite types, distributions and Markov chains

rainbow.math.finite.signed-approximate-fixed-point-sup

Finite types, distributions and Markov chainssrc/rainbow/math/finite/signed_approximate_fixed_point_sup.clj0 definitions, 3 theorems

Finite-sup certificates from pointwise signed approximate fixed points. A whole-carrier two-sided additive epsilon bound implies a signed-distance bound at every enumerated state and therefore a finite sup-residual bound. The existential bridge preserves the same witness, turning a pointwise approximate fixed-point existence theorem into a scalar certificate suitable for an independent verifier. No carrier-exhaustiveness premise is needed: the input already quantifies over every state, while the output deliberately measures only the declared finite source. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.bellman-signed-approximate-optimality-genericmath.finite.signed-sup-distancemath.rational.signed.additive-distance

metric/finite-signed-sup-distance-bounded-by-pointwise-additive-closeness.{u} :
  (S : Type u) (source : Finset S) (left right : S → ℚ) (epsilon : ℚ)
  (epsilon-nonnegative : 0 ≤ epsilon)
  (pointwise-close : ∀ (state : S), proposition/conjunction (left state ≤ right state + epsilon) (right state ≤ left state + epsilon))
  → metric/finite-signed-sup-distance S source left right ≤ epsilon

value/signed-pointwise-approximate-fixed-point-sup-certificate.{u} :
  (S : Type u) (source : Finset S) (operator : (S → ℚ) → S → ℚ) (candidate : S → ℚ)
  (epsilon : ℚ)
  (epsilon-nonnegative : 0 ≤ epsilon)
  (pointwise-close : ∀ (state : S), proposition/conjunction (candidate state ≤ operator candidate state + epsilon) (operator candidate state ≤ candidate state + epsilon))
  → metric/finite-signed-sup-distance S source candidate (operator candidate) ≤ epsilon

value/signed-pointwise-approximate-fixed-point-existence-gives-sup-existence.{u} :
  (S : Type u) (source : Finset S) (operator : (S → ℚ) → S → ℚ) (epsilon : ℚ)
  (epsilon-nonnegative : 0 ≤ epsilon)
  (pointwise-exists : proposition/existence (S → ℚ) (fun candidate => ∀ (state : S), proposition/conjunction (candidate state ≤ operator candidate state + epsilon) (operator candidate state ≤ candidate state + epsilon)))
  → proposition/existence (S → ℚ) (fun candidate => distance candidate (operator candidate) ≤ epsilon)
  where distance := metric/finite-signed-sup-distance S source