Finite Stochastic MDP Proofs

This module proves the key discounted Bellman facts for TorchLean's finite stochastic MDP layer:

• monotonicity of Bellman expectation and Bellman optimality,
• Bellman expectation is a contraction in the sup metric,
• Bellman optimality is also a contraction in the sup metric.

The setting is intentionally finite and concrete. The goal is not maximal generality; it is a clean, trustworthy formal base that mirrors the standard textbook RL theory for discounted MDPs.

References:

• Puterman, Markov Decision Processes (1994), discounted case: https://onlinelibrary.wiley.com/doi/book/10.1002/9780470316887
• Bertsekas, Dynamic Programming and Optimal Control, Vol. 1 (contraction mapping argument): http://web.mit.edu/dimitrib/www/dpoc.html
• Sutton and Barto, Reinforcement Learning: An Introduction (2nd ed., 2018), Bellman expectation/optimality operators: http://incompleteideas.net/book/the-book-2nd.html

noncomputable def Proofs.RL.FiniteStochastic.valueSupDist {nStates : ℕ} [Fact (0 < nStates)] (values₁ values₂ : Spec.RL.ValueFunction ℝ nStates) : ℝ

Sup distance on finite value functions, using the maximum absolute pointwise difference.

theorem Proofs.RL.FiniteStochastic.valueSupDist_nonneg {nStates : ℕ} [Fact (0 < nStates)] (values₁ values₂ : Spec.RL.ValueFunction ℝ nStates) : 0 ≤ valueSupDist values₁ values₂

The sup distance is nonnegative.

theorem Proofs.RL.FiniteStochastic.abs_sub_valueAt_le_valueSupDist {nStates : ℕ} [Fact (0 < nStates)] (values₁ values₂ : Spec.RL.ValueFunction ℝ nStates) (state : Fin nStates) : |Spec.RL.valueAt values₁ state - Spec.RL.valueAt values₂ state| ≤ valueSupDist values₁ values₂

Every pointwise absolute difference is bounded by the sup distance.

theorem Proofs.RL.FiniteStochastic.expectedNextValue_monotone {nStates nActions : ℕ} (mdp : Spec.RL.FiniteStochastic.MDP nStates nActions) (valid : Spec.RL.FiniteStochastic.Valid mdp) (values₁ values₂ : Spec.RL.ValueFunction ℝ nStates) (hValues : ∀ (state : Fin nStates), Spec.RL.valueAt values₁ state ≤ Spec.RL.valueAt values₂ state) (state : Fin nStates) (action : Fin nActions) : Spec.RL.FiniteStochastic.expectedNextValue mdp values₁ state action ≤ Spec.RL.FiniteStochastic.expectedNextValue mdp values₂ state action

Expected next-state value is monotone in the candidate value function.

theorem Proofs.RL.FiniteStochastic.actionValue_monotone {nStates nActions : ℕ} (mdp : Spec.RL.FiniteStochastic.MDP nStates nActions) (valid : Spec.RL.FiniteStochastic.Valid mdp) (values₁ values₂ : Spec.RL.ValueFunction ℝ nStates) (hValues : ∀ (state : Fin nStates), Spec.RL.valueAt values₁ state ≤ Spec.RL.valueAt values₂ state) (state : Fin nStates) (action : Fin nActions) : Spec.RL.FiniteStochastic.actionValue mdp values₁ state action ≤ Spec.RL.FiniteStochastic.actionValue mdp values₂ state action

Bellman state-action values are monotone in the candidate value function.

theorem Proofs.RL.FiniteStochastic.bellmanPolicy_monotone {nStates nActions : ℕ} (mdp : Spec.RL.FiniteStochastic.MDP nStates nActions) (valid : Spec.RL.FiniteStochastic.Valid mdp) (policy : Spec.RL.Policy nStates nActions) (values₁ values₂ : Spec.RL.ValueFunction ℝ nStates) (hValues : ∀ (state : Fin nStates), Spec.RL.valueAt values₁ state ≤ Spec.RL.valueAt values₂ state) (state : Fin nStates) : Spec.RL.valueAt (Spec.RL.FiniteStochastic.bellmanPolicy mdp policy values₁) state ≤ Spec.RL.valueAt (Spec.RL.FiniteStochastic.bellmanPolicy mdp policy values₂) state

Bellman expectation operators are pointwise monotone.

theorem Proofs.RL.FiniteStochastic.bellmanOptimality_monotone {nStates nActions : ℕ} [Fact (0 < nActions)] (mdp : Spec.RL.FiniteStochastic.MDP nStates nActions) (valid : Spec.RL.FiniteStochastic.Valid mdp) (values₁ values₂ : Spec.RL.ValueFunction ℝ nStates) (hValues : ∀ (state : Fin nStates), Spec.RL.valueAt values₁ state ≤ Spec.RL.valueAt values₂ state) (state : Fin nStates) : Spec.RL.valueAt (Spec.RL.FiniteStochastic.bellmanOptimality mdp values₁) state ≤ Spec.RL.valueAt (Spec.RL.FiniteStochastic.bellmanOptimality mdp values₂) state

Optimal Bellman operators are pointwise monotone.

theorem Proofs.RL.FiniteStochastic.expectedNextValue_abs_sub_le {nStates nActions : ℕ} [Fact (0 < nStates)] (mdp : Spec.RL.FiniteStochastic.MDP nStates nActions) (valid : Spec.RL.FiniteStochastic.Valid mdp) (values₁ values₂ : Spec.RL.ValueFunction ℝ nStates) (state : Fin nStates) (action : Fin nActions) : |Spec.RL.FiniteStochastic.expectedNextValue mdp values₁ state action - Spec.RL.FiniteStochastic.expectedNextValue mdp values₂ state action| ≤ valueSupDist values₁ values₂

Coordinatewise expectation difference is bounded by the sup distance.

theorem Proofs.RL.FiniteStochastic.actionValue_abs_sub_le {nStates nActions : ℕ} [Fact (0 < nStates)] (mdp : Spec.RL.FiniteStochastic.MDP nStates nActions) (valid : Spec.RL.FiniteStochastic.Valid mdp) (values₁ values₂ : Spec.RL.ValueFunction ℝ nStates) (state : Fin nStates) (action : Fin nActions) : |Spec.RL.FiniteStochastic.actionValue mdp values₁ state action - Spec.RL.FiniteStochastic.actionValue mdp values₂ state action| ≤ mdp.discount * valueSupDist values₁ values₂

State-action Bellman values are Lipschitz with constant γ in the sup metric.

theorem Proofs.RL.FiniteStochastic.bellmanPolicy_contraction {nStates nActions : ℕ} [Fact (0 < nStates)] (mdp : Spec.RL.FiniteStochastic.MDP nStates nActions) (valid : Spec.RL.FiniteStochastic.Valid mdp) (policy : Spec.RL.Policy nStates nActions) (values₁ values₂ : Spec.RL.ValueFunction ℝ nStates) : valueSupDist (Spec.RL.FiniteStochastic.bellmanPolicy mdp policy values₁) (Spec.RL.FiniteStochastic.bellmanPolicy mdp policy values₂) ≤ mdp.discount * valueSupDist values₁ values₂

Bellman expectation is a contraction with modulus γ in the sup metric:

valueSupDist (T^π values₁) (T^π values₂) ≤ γ * valueSupDist values₁ values₂.

theorem Proofs.RL.FiniteStochastic.actionValue_le_bellmanOptimality {nStates nActions : ℕ} [Fact (0 < nActions)] (mdp : Spec.RL.FiniteStochastic.MDP nStates nActions) (values : Spec.RL.ValueFunction ℝ nStates) (state : Fin nStates) (action : Fin nActions) : Spec.RL.FiniteStochastic.actionValue mdp values state action ≤ Spec.RL.valueAt (Spec.RL.FiniteStochastic.bellmanOptimality mdp values) state

Every particular action-value is bounded by Bellman optimality.

theorem Proofs.RL.FiniteStochastic.bellmanPolicy_le_bellmanOptimality {nStates nActions : ℕ} [Fact (0 < nActions)] (mdp : Spec.RL.FiniteStochastic.MDP nStates nActions) (policy : Spec.RL.Policy nStates nActions) (values : Spec.RL.ValueFunction ℝ nStates) (state : Fin nStates) : Spec.RL.valueAt (Spec.RL.FiniteStochastic.bellmanPolicy mdp policy values) state ≤ Spec.RL.valueAt (Spec.RL.FiniteStochastic.bellmanOptimality mdp values) state

Bellman optimality dominates Bellman evaluation under any deterministic policy.

theorem Proofs.RL.FiniteStochastic.bellmanOptimality_abs_sub_le {nStates nActions : ℕ} [Fact (0 < nStates)] [Fact (0 < nActions)] (mdp : Spec.RL.FiniteStochastic.MDP nStates nActions) (valid : Spec.RL.FiniteStochastic.Valid mdp) (values₁ values₂ : Spec.RL.ValueFunction ℝ nStates) (state : Fin nStates) : |Spec.RL.valueAt (Spec.RL.FiniteStochastic.bellmanOptimality mdp values₁) state - Spec.RL.valueAt (Spec.RL.FiniteStochastic.bellmanOptimality mdp values₂) state| ≤ mdp.discount * valueSupDist values₁ values₂

At a fixed state, Bellman optimality is a contraction with modulus γ.

theorem Proofs.RL.FiniteStochastic.bellmanOptimality_contraction {nStates nActions : ℕ} [Fact (0 < nStates)] [Fact (0 < nActions)] (mdp : Spec.RL.FiniteStochastic.MDP nStates nActions) (valid : Spec.RL.FiniteStochastic.Valid mdp) (values₁ values₂ : Spec.RL.ValueFunction ℝ nStates) : valueSupDist (Spec.RL.FiniteStochastic.bellmanOptimality mdp values₁) (Spec.RL.FiniteStochastic.bellmanOptimality mdp values₂) ≤ mdp.discount * valueSupDist values₁ values₂

Bellman optimality is a contraction with modulus γ in the sup metric:

valueSupDist (T* values₁) (T* values₂) ≤ γ * valueSupDist values₁ values₂.

Contraction Iterates and Fixed Points

The earlier theorems show that (under 0 ≤ γ < 1) the Bellman operators are γ-contractions in the sup metric (valueSupDist).

This section packages the standard consequences used throughout discounted-RL theory:

• iterating a contraction shrinks distances geometrically (γ^k),
• fixed points are unique,
• the error to a fixed point decays geometrically under iteration.

These statements are the formal backbone behind “value iteration converges” style arguments, and they are useful even before we prove existence of a fixed point (existence is typically obtained via a completeness argument, or via an explicit linear-system solution in the finite case).

theorem Proofs.RL.FiniteStochastic.valueSupDist_eq_zero_iff {nStates : ℕ} [Fact (0 < nStates)] (values₁ values₂ : Spec.RL.ValueFunction ℝ nStates) : valueSupDist values₁ values₂ = 0 ↔ values₁ = values₂

valueSupDist = 0 iff two finite value functions are equal.

theorem Proofs.RL.FiniteStochastic.bellmanPolicy_iterate_contraction {nStates nActions : ℕ} [Fact (0 < nStates)] (mdp : Spec.RL.FiniteStochastic.MDP nStates nActions) (valid : Spec.RL.FiniteStochastic.Valid mdp) (policy : Spec.RL.Policy nStates nActions) (k : ℕ) (values₁ values₂ : Spec.RL.ValueFunction ℝ nStates) : valueSupDist ((Spec.RL.FiniteStochastic.bellmanPolicy mdp policy)^[k] values₁) ((Spec.RL.FiniteStochastic.bellmanPolicy mdp policy)^[k] values₂) ≤ mdp.discount ^ k * valueSupDist values₁ values₂

bellmanPolicy iterates are geometric contractions in valueSupDist.

theorem Proofs.RL.FiniteStochastic.bellmanPolicy_fixedPoint_unique {nStates nActions : ℕ} [Fact (0 < nStates)] (mdp : Spec.RL.FiniteStochastic.MDP nStates nActions) (valid : Spec.RL.FiniteStochastic.Valid mdp) (policy : Spec.RL.Policy nStates nActions) (v w : Spec.RL.ValueFunction ℝ nStates) (hv : Spec.RL.FiniteStochastic.bellmanPolicy mdp policy v = v) (hw : Spec.RL.FiniteStochastic.bellmanPolicy mdp policy w = w) : v = w

If a discounted Bellman policy operator has a fixed point, it is unique.

This is the standard “contraction has at most one fixed point” argument.

theorem Proofs.RL.FiniteStochastic.bellmanPolicy_iterate_error_to_fixedPoint {nStates nActions : ℕ} [Fact (0 < nStates)] (mdp : Spec.RL.FiniteStochastic.MDP nStates nActions) (valid : Spec.RL.FiniteStochastic.Valid mdp) (policy : Spec.RL.Policy nStates nActions) (v vStar : Spec.RL.ValueFunction ℝ nStates) (hvStar : Spec.RL.FiniteStochastic.bellmanPolicy mdp policy vStar = vStar) (k : ℕ) : valueSupDist ((Spec.RL.FiniteStochastic.bellmanPolicy mdp policy)^[k] v) vStar ≤ mdp.discount ^ k * valueSupDist v vStar

Error bound to a fixed point: iterating the Bellman policy operator reduces sup-distance geometrically (γ^k).

theorem Proofs.RL.FiniteStochastic.bellmanOptimality_iterate_contraction {nStates nActions : ℕ} [Fact (0 < nStates)] [Fact (0 < nActions)] (mdp : Spec.RL.FiniteStochastic.MDP nStates nActions) (valid : Spec.RL.FiniteStochastic.Valid mdp) (k : ℕ) (values₁ values₂ : Spec.RL.ValueFunction ℝ nStates) : valueSupDist ((Spec.RL.FiniteStochastic.bellmanOptimality mdp)^[k] values₁) ((Spec.RL.FiniteStochastic.bellmanOptimality mdp)^[k] values₂) ≤ mdp.discount ^ k * valueSupDist values₁ values₂

bellmanOptimality iterates are geometric contractions in valueSupDist.

theorem Proofs.RL.FiniteStochastic.bellmanOptimality_fixedPoint_unique {nStates nActions : ℕ} [Fact (0 < nStates)] [Fact (0 < nActions)] (mdp : Spec.RL.FiniteStochastic.MDP nStates nActions) (valid : Spec.RL.FiniteStochastic.Valid mdp) (v w : Spec.RL.ValueFunction ℝ nStates) (hv : Spec.RL.FiniteStochastic.bellmanOptimality mdp v = v) (hw : Spec.RL.FiniteStochastic.bellmanOptimality mdp w = w) : v = w

If a discounted Bellman optimality operator has a fixed point, it is unique.

This is the “contraction has at most one fixed point” argument for T*.

theorem Proofs.RL.FiniteStochastic.bellmanOptimality_iterate_error_to_fixedPoint {nStates nActions : ℕ} [Fact (0 < nStates)] [Fact (0 < nActions)] (mdp : Spec.RL.FiniteStochastic.MDP nStates nActions) (valid : Spec.RL.FiniteStochastic.Valid mdp) (v vStar : Spec.RL.ValueFunction ℝ nStates) (hvStar : Spec.RL.FiniteStochastic.bellmanOptimality mdp vStar = vStar) (k : ℕ) : valueSupDist ((Spec.RL.FiniteStochastic.bellmanOptimality mdp)^[k] v) vStar ≤ mdp.discount ^ k * valueSupDist v vStar

Error bound to a fixed point: iterating Bellman optimality reduces sup-distance geometrically.