§3, discounted case (p. 446) — the path of a stationary policy is a sigma, and every sigma is such a path
ProvedMDPComplexity.Discounted.stationary_path_sigmagraph-theorymarkov-decision-processp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1stationary-policy
Consider a finite deterministic stationary Markov decision process with initial state .
- For every stationary policy there is a sigma from whose nodes are the first states generated by , and whose discounted cost equals that of for every : .
- Conversely, for every sigma from there is a stationary policy whose first states are the nodes of and with for every .
Here and is the discounted cost of the infinite walk that follows and repeats its cycle forever. Together with the existence of a stationary optimal policy, this identifies the optimal discounted cost with the least discounted cost of a sigma.
Formalization Note The cost identities are stated for the paper's discount range , where both infinite sums converge.
Preamble
import Mathlib import Definitions.Def_MDPComplexity_Discounted_Model
Formal statement
namespace MDPComplexity.Discounted
theorem stationary_path_sigma {S : Type} [Fintype S] [DecidableEq S] (M : DetMDP S) (s₀ : S) :
(∀ δ : M.Policy, M.IsStationary δ →
∃ P : M.Sigma s₀, (∀ t ≤ P.N, P.w t = M.path s₀ δ t) ∧
∀ β : ℝ, 0 < β ∧ β < 1 → M.discCost β s₀ δ = P.cost β) ∧
(∀ P : M.Sigma s₀, ∃ δ : M.Policy, M.IsStationary δ ∧
(∀ t ≤ P.N, M.path s₀ δ t = P.w t) ∧
∀ β : ℝ, 0 < β ∧ β < 1 → M.discCost β s₀ δ = P.cost β) := by sorry
end MDPComplexity.Discounted
Source
Papadimitriou and Tsitsiklis, The Complexity of Markov Decision Processes, Math. Oper. Res. 12(3) (1987), p. 446, §3, The infinite horizon, discounted case
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.