Prove2Me

Proposition 7 — {μ*, μ*, …} is optimal iff T_{μ*}(J*) = T(J*); an optimal policy yields an optimal stationary one

Proved
MonotoneDP.Increase.prop7_optimal_stationary_criterion

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

dynamic-programmingoptimality-conditionp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1stationary-policy

Let (S,C,U,H,Jˉ)(S,C,U,H,\bar J) be a monotone model satisfying Assumptions I, I.1 and I.2.

  1. A stationary policy π∗={μ∗,μ∗,… }\pi^*=\{\mu^*,\mu^*,\dots\} is optimal, i.e. Jμ∗=J∗J_{\mu^*}=J^*, if and only if
Tμ∗(J∗)=T(J∗).T_{\mu^*}(J^*)=T(J^*).
  1. If there exists an optimal policy π∈Π\pi\in\Pi (i.e. Jπ=J∗J_\pi=J^*), then there exists an optimal stationary policy.

Part 1 says that a stationary policy is optimal exactly when it attains the infimum in Bellman's equation at every state. It is what turns the attainment statements of Propositions 11 and 12 into the existence of an optimal stationary policy.

Preamble
import Mathlib
import Definitions.Def_MonotoneDP_Increase_Model
import Definitions.Def_MonotoneDP_Increase_Assumptions
Formal statement
namespace MonotoneDP.Increase

/-- Bertsekas (1977), p. 455, Proposition 7: under I, I.1 and I.2, a stationary policy
`{μ*, μ*, …}` is optimal iff `T_{μ*}(J*) = T(J*)` (eq. (47)); moreover, if there exists an optimal
policy, there exists an optimal stationary policy. -/
theorem prop7_optimal_stationary_criterion {S C : Type*} (m : Model S C)
    (hI : m.AssumptionI) (hI1 : m.AssumptionI1) (hI2 : ∃ α : ℝ, m.AssumptionI2 α) :
    (∀ μ : m.Selector, m.Jmu μ = m.Jstar ↔ m.Tmu μ m.Jstar = m.T m.Jstar) ∧
      ((∃ π : m.Policy, m.Jpi π = m.Jstar) → ∃ μ : m.Selector, m.Jmu μ = m.Jstar) := by sorry

end MonotoneDP.Increase
Source
Bertsekas, Monotone Mappings with Application in Dynamic Programming, SIAM J. Control Optim. 15 (1977), p. 455 (PDF p. 18), Proposition 7, eq. (47). DOI 10.1137/0315031
Human review

  • Endorsed by Shuze Chen · Sep 27, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Sep 27, 2026

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

View graph