The transformed discounted value solves the original average cost equation

Proved

ArapostathisAC.RossReduction.rewritten_acoe

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

average-cost-optimality-equationdiscounted-costp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $\widetilde M$ have the same admissible actions and bounded nonnegative costs as $M$ , and let its transition law be the transformation in Theorem 5.6 for $0<\alpha<1$ . Write $\widetilde J^*_{1-\alpha}$ for its discounted value. Every value $\widetilde J^*_{1-\alpha}(i)$ is finite, and the value function is bounded. Moreover, with $h(i)=\widetilde J^*_{1-\alpha}(i)$ and $\rho=\alpha\widetilde J^*_{1-\alpha}(0)$ ,

\rho+h(i)=\min_{a\in U(i)}\left\{c(i,a)+\sum_{j\in S}P(j\mid i,a)h(j)\right\}\qquad(i\in S).

This is the equation at the center of the reduction from average cost for $M$ to discounting for $\widetilde M$ .

Formalization Note The minimum is attained, and the real expectation series is summable. The explicit finiteness conclusion prevents conversion of an infinite discounted value to Lean's default real value zero. The cost bound comes from §5.1.

Preamble

import Mathlib
import Definitions.Def_ArapostathisAC_RossReduction_CMP

Formal statement

namespace ArapostathisAC.RossReduction

/-- The discounted optimality equation for the transformed process,
rewritten as the original process's average cost optimality equation. -/
theorem rewritten_acoe {A : Type*} [MetricSpace A] [MeasurableSpace A] [BorelSpace A]
    (M M' : CMP A) (α : ℝ) (hα : 0 < α) (hα1 : α < 1)
    (hP : ∀ i, ∀ a ∈ M.U i, α ≤ prob M i a 0)
    (hmod : ModifiedLaw M M' α)
    (C : ℝ) (hc : ∀ i, ∀ a ∈ M.U i, M.c i a ≤ C) :
    (∀ i, discValue M' (1 - α) i ≠ ⊤) ∧
    (∃ B : ℝ, ∀ i, |(discValue M' (1 - α) i).toReal| ≤ B) ∧
    ACOE M (α * (discValue M' (1 - α) 0).toReal)
      (fun i => (discValue M' (1 - α) i).toReal) := by sorry

end ArapostathisAC.RossReduction

Source

Arapostathis et al., Discrete-time controlled Markov processes with average cost criterion: a survey, SIAM J. Control Optim. 31(2) (1993), p. 304, displayed ACOE in proof of Theorem 5.6; https://doi.org/10.1137/0331018

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph