No policy improves on the least reachable cycle mean
ProvedMDPComplexity.AverageCost.no_better_policyaverage-costcyclesdeterministicp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1
Let be a reachable simple cycle of least mean cost among all reachable simple cycles of a finite stationary deterministic process. For every state-and-time policy , even if its finite averages fail to converge,
This gives the lower-bound half of the cycle characterization, including arbitrary nonstationary policies.
Formalization Note The paper's phrase “this cannot be improved” is stated using the lower limit; this also establishes the claim for its upper-limit reading of average cost.
Preamble
import Definitions.Def_MDPComplexity_AverageCost_Model
Formal statement
namespace MDPComplexity.AverageCost
open Filter
variable {S : Type*} [Fintype S] [DecidableEq S]
/-- §3, p. 446: no policy can improve on the least reachable cycle mean.
The lower limit makes the assertion valid even when a policy's averages oscillate. -/
theorem no_better_policy (M : DetMDP S) (s₀ : S) :
∀ (δ : M.Policy) (C₀ : M.Cycle),
M.Reachable s₀ C₀.base →
(∀ C : M.Cycle, M.Reachable s₀ C.base → C₀.mean ≤ C.mean) →
C₀.mean ≤ liminf (M.average s₀ δ) atTop := 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.