Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-signed-transition-bridge

Finite types, distributions and Markov chainssrc/rainbow/math/finite/bellman_signed_transition_bridge.clj0 definitions, 5 theorems

Embed ordinary nonnegative transition kernels into signed Bellman proofs. The Grothendieck embedding preserves a finite map-sum, so an nnrat row whose total mass is one becomes a nonnegative normalized signed row. The final theorem packages those bridge facts around the signed Bellman optimality contraction: callers may provide the natural nnrat transition kernel and its nnrat normalization proof, while rewards and value functions remain signed. This is the model-level refinement boundary needed by practical MDP data. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.bellman-signed-optimal-contraction

signed/map-sum-from-nnrat.{u} :
  (A : Type u) (mapping : A → ℚ≥0) (items : List A)
  → Σ item∈items, signed/from-nnrat (mapping item) = signed/from-nnrat (nnrat/map-sum A mapping items)

probability/signed-total-mass-from-nnrat.{u} :
  (A : Type u) (source : Finset A) (mass : A → ℚ≥0)
  → probability/signed-total-mass A source (fun item => signed/from-nnrat (mass item)) = signed/from-nnrat (probability/nnrat-total-mass A source mass)

probability/signed-embedded-mass-nonnegative.{u} :
  (A : Type u) (mass : A → ℚ≥0) (item : A)
  → 0 ≤ signed/from-nnrat (mass item)

probability/signed-total-mass-normalized-from-nnrat.{u} :
  (A : Type u) (source : Finset A) (mass : A → ℚ≥0)
  (normalized : probability/nnrat-total-mass A source mass = 1)
  → probability/signed-total-mass A source (fun item => signed/from-nnrat (mass item)) = 1

value/nnrat-transition-signed-optimality-step-additively-contractive.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (actions : Finset A)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ) (discount : ℚ≥0)
  (fallback : S → A)
  (fallback-admissible : ∀ (state : S), fallback state ∈ actions)
  (normalized : ∀ (state : S), ∀ (action : A), probability/nnrat-total-mass S states (transition state action) = 1)
  (left-value right-value : S → ℚ) (epsilon : ℚ)
  (left-pointwise : ∀ (state : S), left-value state ≤ right-value state + epsilon)
  (right-pointwise : ∀ (state : S), right-value state ≤ left-value state + epsilon)
  (state : S)
  → proposition/conjunction (step₁ ≤ step + signed/from-nnrat discount · epsilon) (step ≤ step₁ + signed/from-nnrat discount · epsilon)
  where step := value/signed-optimality-step S A actions fallback (fun value => fun state₁ => fun action => bellman/signed-action-backup S A states (fun state₂ => fun action₁ => fun next-state => signed/from-nnrat (transition state₂ action₁ next-state)) reward (signed/from-nnrat discount) value state₁ action) right-value state
  where step₁ := value/signed-optimality-step S A actions fallback (fun value => fun state₁ => fun action => bellman/signed-action-backup S A states (fun state₂ => fun action₁ => fun next-state => signed/from-nnrat (transition state₂ action₁ next-state)) reward (signed/from-nnrat discount) value state₁ action) left-value state