Finite-MDP Proofs

This module proves the first foundational theorems for TorchLean's finite discounted MDP layer:

• Bellman policy operators are monotone for nonnegative discounts,
• Bellman optimality operators dominate every policy operator,
• Bellman optimality is itself monotone,
• Bellman policy and Bellman optimality are contractions in the finite sup metric.

The proofs begin with deterministic finite MDPs, giving a trustworthy base before stochastic transitions or richer measure-theoretic machinery.

References:

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

Sup Metric for Finite Value Tables

The metric is the maximum absolute pointwise difference between two value tables, and it is defined once here for both finite developments: Proofs.RL.FiniteStochastic opens these three declarations rather than restating them. This module owns them because the specs already put Spec.RL.MDP underneath Spec.RL.FiniteStochasticMDP, so the deterministic side is the more basic of the two.

Do not confuse this with Proofs.RL.Markov.valueSupDist, which measures the same thing on a possibly-infinite state space. That one is an sSup rather than a Finset.sup', so it needs a boundedness hypothesis before any of these facts hold, and the two cannot share an implementation. The contraction argument itself is standard: see Puterman, Markov Decision Processes (1994), and Bertsekas, Dynamic Programming and Optimal Control, Vol. 1.

noncomputable def Proofs.RL.MDP.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.MDP.valueSupDist_nonneg {nStates : ℕ} [Fact (0 < nStates)] (values₁ values₂ : Spec.RL.ValueFunction ℝ nStates) : 0 ≤ valueSupDist values₁ values₂

The sup distance is nonnegative.

theorem Proofs.RL.MDP.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.MDP.stateActionValue_eq {nStates nActions : ℕ} (mdp : Spec.RL.FiniteMDP ℝ nStates nActions) (values : Spec.RL.ValueFunction ℝ nStates) (state : Fin nStates) (action : Fin nActions) : Spec.RL.stateActionValue mdp values state action = have out := mdp.step state action; out.reward + mdp.discount * Spec.RL.continueMask out.terminated * Spec.RL.valueAt values out.state

stateActionValue is exactly the Bellman backup on the chosen successor state.

theorem Proofs.RL.MDP.valueAt_bellmanPolicy {nStates nActions : ℕ} (mdp : Spec.RL.FiniteMDP ℝ nStates nActions) (policy : Spec.RL.Policy nStates nActions) (values : Spec.RL.ValueFunction ℝ nStates) (state : Fin nStates) : Spec.RL.valueAt (Spec.RL.bellmanPolicy mdp policy values) state = Spec.RL.stateActionValue mdp values state (policy state)

Policy Bellman operators read back exactly the selected state-action value.

theorem Proofs.RL.MDP.continueMask_nonneg (done : Bool) : 0 ≤ Spec.RL.continueMask done

continueMask is always nonnegative.

theorem Proofs.RL.MDP.stateActionValue_monotone {nStates nActions : ℕ} (mdp : Spec.RL.FiniteMDP ℝ nStates nActions) (values₁ values₂ : Spec.RL.ValueFunction ℝ nStates) (hγ : 0 ≤ mdp.discount) (hValues : ∀ (state : Fin nStates), Spec.RL.valueAt values₁ state ≤ Spec.RL.valueAt values₂ state) (state : Fin nStates) (action : Fin nActions) : Spec.RL.stateActionValue mdp values₁ state action ≤ Spec.RL.stateActionValue mdp values₂ state action

A Bellman state-action value is monotone in the candidate value function when γ ≥ 0.

theorem Proofs.RL.MDP.bellmanPolicy_monotone {nStates nActions : ℕ} (mdp : Spec.RL.FiniteMDP ℝ nStates nActions) (policy : Spec.RL.Policy nStates nActions) (values₁ values₂ : Spec.RL.ValueFunction ℝ nStates) (hγ : 0 ≤ mdp.discount) (hValues : ∀ (state : Fin nStates), Spec.RL.valueAt values₁ state ≤ Spec.RL.valueAt values₂ state) (state : Fin nStates) : Spec.RL.valueAt (Spec.RL.bellmanPolicy mdp policy values₁) state ≤ Spec.RL.valueAt (Spec.RL.bellmanPolicy mdp policy values₂) state

Bellman policy operators are pointwise monotone for nonnegative discounts.

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

Bellman optimality dominates every particular action.

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

Bellman optimality dominates Bellman evaluation under any deterministic policy.

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

Bellman optimality is pointwise monotone for nonnegative discounts.

Contraction Guarantees

For 0 ≤ γ < 1, deterministic finite Bellman operators are contractions in valueSupDist. This is the same mathematical guarantee used by value iteration in the stochastic layer; the only difference is that the next state is a single successor instead of an expectation over a transition row.

theorem Proofs.RL.MDP.stateActionValue_abs_sub_le {nStates nActions : ℕ} [Fact (0 < nStates)] (mdp : Spec.RL.FiniteMDP ℝ nStates nActions) (values₁ values₂ : Spec.RL.ValueFunction ℝ nStates) (hγ₀ : 0 ≤ mdp.discount) (state : Fin nStates) (action : Fin nActions) : |Spec.RL.stateActionValue mdp values₁ state action - Spec.RL.stateActionValue mdp values₂ state action| ≤ mdp.discount * valueSupDist values₁ values₂

Deterministic state-action Bellman values are Lipschitz with constant γ.

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

Bellman evaluation for a deterministic policy is a γ-contraction in the finite sup metric.

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

At a fixed state, Bellman optimality is Lipschitz with constant γ.

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

Bellman optimality is a γ-contraction in the finite sup metric.