Finite-MDP Proofs #
This module proves the 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,
- for
γ < 1both have a unique fixed point, and value iteration converges to it.
The fixed-point facts are proved once, for any operator on finite value tables that contracts the
sup distance (SupContraction). They come from Mathlib's Banach fixed-point theorem
(ContractingWith.fixedPoint) after carrying value tables to Fin n → ℝ, whose metric is the sup
metric. Proofs.RL.FiniteStochastic reuses the same development for stochastic transitions.
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. The finite stochastic development opens these declarations rather than restating them.
Proofs.RL.Markov.valueSupDist 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.
Value tables as functions Fin n → ℝ. Mathlib's metric on that type is the sup metric.
Instances For
Sup distance on finite value functions, using the maximum absolute pointwise difference.
Instances For
Every pointwise absolute difference is bounded by the sup distance.
The sup distance is nonnegative.
A uniform bound on pointwise differences bounds the sup distance.
valueSupDist is Mathlib's sup distance on Fin n → ℝ.
valueSupDist = 0 iff two finite value functions are equal.
Fixed Points of Sup-Norm Contractions #
Everything here holds for any operator T on finite value tables with
valueSupDist (T v) (T w) ≤ γ * valueSupDist v w and 0 ≤ γ < 1. Conjugating T by valueEquiv
gives a ContractingWith map on the complete space Fin n → ℝ, and the conclusions are Mathlib's.
T contracts the finite sup distance by the factor γ ∈ [0, 1).
The factor is nonnegative.
The factor is strictly below one.
- dist_le (values₁ values₂ : Spec.RL.ValueFunction ℝ nStates) : valueSupDist (T values₁) (T values₂) ≤ γ * valueSupDist values₁ values₂
One application of
Tshrinks every sup distance byγ.
Instances For
The operator T read on Fin n → ℝ is a Mathlib ContractingWith map.
The fixed point of T given by Banach's fixed-point theorem.
Instances For
fixedPoint is a fixed point.
Every fixed point of T is fixedPoint.
T has exactly one fixed point.
k applications of T shrink every sup distance by γ ^ k.
The distance from the k-th iterate to any fixed point decays like γ ^ k.
A priori error bound for value iteration, computable from the first step alone.
Value iteration converges to the fixed point from any starting table.
Deterministic Bellman Operators #
Policy Bellman operators read back exactly the selected state-action value.
Bellman optimality reads back the best state-action value.
A Bellman state-action value is monotone in the candidate value function when γ ≥ 0.
Bellman policy operators are pointwise monotone for nonnegative discounts.
Bellman optimality dominates every particular action.
Bellman optimality dominates Bellman evaluation under any deterministic policy.
Bellman optimality is pointwise monotone for nonnegative discounts.
Deterministic state-action Bellman values are Lipschitz with constant γ.
Bellman evaluation for a deterministic policy is a γ-contraction in the finite sup metric.
At a fixed state, Bellman optimality is Lipschitz with constant γ.
Bellman optimality is a γ-contraction in the finite sup metric.
For 0 ≤ γ < 1, policy evaluation is a SupContraction: it has a unique fixed point and
value iteration converges to it.
For 0 ≤ γ < 1, Bellman optimality is a SupContraction: the optimal value table exists, is
unique, and value iteration converges to it.