Following a reachable cycle forever attains its mean cost
ProvedMDPComplexity.AverageCost.follow_cycleaverage-costcyclesdeterministicp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1
Let be a finite stationary deterministic Markov decision process, an initial state and a simple cycle whose starting state can be reached from . There is a state-and-time policy whose finite averages converge to the cycle mean:
This is the attainment half of the paper's reduction of average-cost optimization to reachable cycles.
Formalization Note A cycle retains its decision arcs, including parallel arcs and loops. Its states are distinct; the initial finite walk can have repeated states. At the finite average is set to zero, with no effect on convergence.
Preamble
import Definitions.Def_MDPComplexity_AverageCost_Model
Formal statement
namespace MDPComplexity.AverageCost
open Filter
variable {S : Type*} [Fintype S] [DecidableEq S]
/-- §3, p. 446: an infinite path which reaches a cycle and follows it forever
has limiting average cost equal to that cycle's mean. -/
theorem follow_cycle (M : DetMDP S) (s₀ : S) :
∀ C : M.Cycle, M.Reachable s₀ C.base →
∃ δ : M.Policy, Tendsto (M.average s₀ δ) atTop (nhds C.mean) := by sorry
end MDPComplexity.AverageCost
Source
Papadimitriou and Tsitsiklis, The Complexity of Markov Decision Processes, Math. Oper. Res. 12(3) (1987), p. 446, §3 The infinite horizon undiscounted case, proof of Theorem 3, https://doi.org/10.1287/moor.12.3.441
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.