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,
• both operators have a unique fixed point, and value iteration converges to it geometrically.

The setting is intentionally finite and concrete: a clean, trustworthy formal base that mirrors the standard textbook RL theory for discounted MDPs, rather than maximal generality.

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

The sup metric and the fixed-point theory come from Proofs.RL.MDP, which proves them once for any SupContraction on finite value tables. This file only proves the one-step bounds for stochastic transitions. The open is fully qualified because MDP on its own is also the name of the transition structure used below.

theorem Proofs.RL.FiniteStochastic.valueAt_bellmanPolicy {nStates 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.FiniteStochastic.actionValue mdp values state (policy state)

Policy evaluation reads back the selected action value.

theorem Proofs.RL.FiniteStochastic.valueAt_bellmanOptimality {nStates nActions : ℕ} [Fact (0 < nActions)] (mdp : Spec.RL.FiniteStochastic.MDP nStates nActions) (values : Spec.RL.ValueFunction ℝ nStates) (state : Fin nStates) : have x := ⋯; Spec.RL.valueAt (Spec.RL.FiniteStochastic.bellmanOptimality mdp values) state = Finset.univ.sup' ⋯ (Spec.RL.FiniteStochastic.actionValue mdp values state)

Bellman optimality reads back the best action value.

theorem Proofs.RL.FiniteStochastic.expectedNextValue_mono {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_mono {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_mono {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_mono {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| ≤ MDP.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 * MDP.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) : MDP.valueSupDist (Spec.RL.FiniteStochastic.bellmanPolicy mdp policy values₁) (Spec.RL.FiniteStochastic.bellmanPolicy mdp policy values₂) ≤ mdp.discount * MDP.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 * MDP.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) : MDP.valueSupDist (Spec.RL.FiniteStochastic.bellmanOptimality mdp values₁) (Spec.RL.FiniteStochastic.bellmanOptimality mdp values₂) ≤ mdp.discount * MDP.valueSupDist values₁ values₂

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

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

Fixed Points and Value Iteration

Valid puts the discount in [0, 1), so both operators are SupContractions. The fixed point exists by Banach's theorem, is unique, and value iteration converges to it from any start. The theorems below name the consequences most often cited.

theorem Proofs.RL.FiniteStochastic.bellmanPolicy_supContraction {nStates nActions : ℕ} [Fact (0 < nStates)] (mdp : Spec.RL.FiniteStochastic.MDP nStates nActions) (valid : Spec.RL.FiniteStochastic.Valid mdp) (policy : Spec.RL.Policy nStates nActions) : MDP.SupContraction mdp.discount (Spec.RL.FiniteStochastic.bellmanPolicy mdp policy)

Policy evaluation is a SupContraction.

theorem Proofs.RL.FiniteStochastic.bellmanOptimality_supContraction {nStates nActions : ℕ} [Fact (0 < nStates)] [Fact (0 < nActions)] (mdp : Spec.RL.FiniteStochastic.MDP nStates nActions) (valid : Spec.RL.FiniteStochastic.Valid mdp) : MDP.SupContraction mdp.discount (Spec.RL.FiniteStochastic.bellmanOptimality mdp)

Bellman optimality is a SupContraction.

theorem Proofs.RL.FiniteStochastic.bellmanPolicy_existsUnique_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) : ∃! values : Spec.RL.ValueFunction ℝ nStates, Spec.RL.FiniteStochastic.bellmanPolicy mdp policy values = values

The value of a policy exists and is unique: T^π has exactly one fixed point.

theorem Proofs.RL.FiniteStochastic.bellmanOptimality_existsUnique_fixedPoint {nStates nActions : ℕ} [Fact (0 < nStates)] [Fact (0 < nActions)] (mdp : Spec.RL.FiniteStochastic.MDP nStates nActions) (valid : Spec.RL.FiniteStochastic.Valid mdp) : ∃! values : Spec.RL.ValueFunction ℝ nStates, Spec.RL.FiniteStochastic.bellmanOptimality mdp values = values

The optimal value function exists and is unique: T* has exactly one fixed point.

theorem Proofs.RL.FiniteStochastic.bellmanOptimality_valueIteration_tendsto {nStates nActions : ℕ} [Fact (0 < nStates)] [Fact (0 < nActions)] (mdp : Spec.RL.FiniteStochastic.MDP nStates nActions) (valid : Spec.RL.FiniteStochastic.Valid mdp) (values : Spec.RL.ValueFunction ℝ nStates) : Filter.Tendsto (fun (k : ℕ) => MDP.valueSupDist ((Spec.RL.FiniteStochastic.bellmanOptimality mdp)^[k] values) ⋯.fixedPoint) Filter.atTop (nhds 0)

Value iteration converges to the optimal value function from any starting table.

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) : MDP.valueSupDist ((Spec.RL.FiniteStochastic.bellmanPolicy mdp policy)^[k] values₁) ((Spec.RL.FiniteStochastic.bellmanPolicy mdp policy)^[k] values₂) ≤ mdp.discount ^ k * MDP.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

A fixed point of the Bellman policy operator is unique.

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 : ℕ) : MDP.valueSupDist ((Spec.RL.FiniteStochastic.bellmanPolicy mdp policy)^[k] v) vStar ≤ mdp.discount ^ k * MDP.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) : MDP.valueSupDist ((Spec.RL.FiniteStochastic.bellmanOptimality mdp)^[k] values₁) ((Spec.RL.FiniteStochastic.bellmanOptimality mdp)^[k] values₂) ≤ mdp.discount ^ k * MDP.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

A fixed point of the Bellman optimality operator is unique.

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 : ℕ) : MDP.valueSupDist ((Spec.RL.FiniteStochastic.bellmanOptimality mdp)^[k] v) vStar ≤ mdp.discount ^ k * MDP.valueSupDist v vStar

Error bound to a fixed point: iterating Bellman optimality shrinks the sup distance geometrically.