Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

§3, discounted case (p. 446) — the path of a stationary policy is a sigma, and every sigma is such a path

Proved
MDPComplexity.Discounted.stationary_path_sigma

by mikedeng1 · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

graph-theorymarkov-decision-processp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1stationary-policy

Consider a finite deterministic stationary Markov decision process with initial state s0s_0s0​.

  1. For every stationary policy δ\deltaδ there is a sigma PPP from s0s_0s0​ whose nodes w0,…,wNw_0,\dots,w_Nw0​,…,wN​ are the first N+1N+1N+1 states s0,…,sNs_0,\dots,s_Ns0​,…,sN​ generated by δ\deltaδ, and whose discounted cost equals that of δ\deltaδ for every 0<β<10<\beta<10<β<1: Jβ(δ)=cβ(P)J_\beta(\delta)=c_\beta(P)Jβ​(δ)=cβ​(P).
  2. Conversely, for every sigma PPP from s0s_0s0​ there is a stationary policy δ\deltaδ whose first N+1N+1N+1 states are the nodes w0,…,wNw_0,\dots,w_Nw0​,…,wN​ of PPP and with Jβ(δ)=cβ(P)J_\beta(\delta)=c_\beta(P)Jβ​(δ)=cβ​(P) for every 0<β<10<\beta<10<β<1.

Here Jβ(δ)=∑t≥0βtc(st,δ(st,t))J_\beta(\delta)=\sum_{t\ge0}\beta^tc(s_t,\delta(s_t,t))Jβ​(δ)=∑t≥0​βtc(st​,δ(st​,t)) and cβ(P)c_\beta(P)cβ​(P) is the discounted cost of the infinite walk that follows PPP 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 0<β<10<\beta<10<β<1, 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
  • Endorsed by Shuze Chen · Oct 6, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 6, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me