Prove2Me

Proposition 6 — Bellman's equation J* = T(J*) and maximality of J* under D and D.1

Proved
MonotoneDP.Decrease.prop6_bellman_equation

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

bellman-equationdynamic-programmingp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1

In the abstract dynamic programming model of Bertsekas (1977), with T(J)(x)=inf⁡u∈U(x)H(x,u,J)T(J)(x)=\inf_{u\in U(x)}H(x,u,J) and optimal value function J∗=inf⁡π∈ΠJπJ^*=\inf_{\pi\in\Pi}J_\pi, suppose Assumptions D and D.1 hold. Then J∗J^* satisfies Bellman's equation

J∗=T(J∗).J^*=T(J^*).

Furthermore, if J′∈FJ'\in F satisfies J′≤JˉJ'\le\bar J and J′≤T(J′)J'\le T(J'), then J′≤J∗J'\le J^*.

So under uniform decrease J∗J^* is the largest fixed point, and indeed the largest sub-solution below Jˉ\bar J, of the Bellman operator. It is the counterpart under D of the Bellman equation proved under Assumption I.

Formalization Note All inequalities between functions are pointwise, in [−∞,∞][-\infty,\infty].

Preamble
import Mathlib
import Definitions.Def_MonotoneDP_Decrease_Model
import Definitions.Def_MonotoneDP_Decrease_Assumptions
Formal statement
namespace MonotoneDP.Decrease

/-- Bertsekas (1977), p. 453, Proposition 6: under D and D.1, `J* = T(J*)`; moreover every
`J' ∈ F` with `J' ≤ J̄` and `J' ≤ T(J')` satisfies `J' ≤ J*`. -/
theorem prop6_bellman_equation {S C : Type*} (m : Model S C)
    (hD : m.AssumptionD) (hD1 : m.AssumptionD1) :
    m.Jstar = m.T m.Jstar ∧
      ∀ J' : S → EReal, J' ≤ m.Jbar → J' ≤ m.T J' → J' ≤ m.Jstar := by sorry

end MonotoneDP.Decrease
Source
Bertsekas, Monotone Mappings with Application in Dynamic Programming, SIAM J. Control Optim. 15 (1977), p. 453 (PDF p. 16), Proposition 6. 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