The transformed transition law defines a controlled Markov process

Proved

ArapostathisAC.RossReduction.modified_exists

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

controlled-markov-processp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1transition-kernel

Let $M$ be a countable-state controlled Markov process. Suppose $0<\alpha<1$ and $P(0\mid i,a)\ge\alpha$ for every admissible state-action pair. Then there is a controlled Markov process $\widetilde M$ with the same admissible actions and costs as $M$ and with transition law

\widetilde P(j\mid i,a)=\frac{P(j\mid i,a)-\alpha\mathbf 1_{\{j=0\}}}{1-\alpha}.

This establishes that the transition probabilities used in Theorem 5.6's reduction form a genuine stochastic law, while preserving the standing measurability and continuity conditions.

Formalization Note The paper states $\alpha>0$ ; its displayed transformation divides by $1-\alpha$ , so this item explicitly requires $\alpha<1$ . The equation is imposed on admissible pairs only, the domain on which the paper defines the process.

Preamble

import Mathlib
import Definitions.Def_ArapostathisAC_RossReduction_CMP

Formal statement

namespace ArapostathisAC.RossReduction

/-- The transition law displayed in the proof of Theorem 5.6 defines a CMP
with the original admissible actions and cost. -/
theorem modified_exists {A : Type*} [MetricSpace A] [MeasurableSpace A] [BorelSpace A]
    (M : CMP A) (α : ℝ) (hα : 0 < α) (hα1 : α < 1)
    (hP : ∀ i, ∀ a ∈ M.U i, α ≤ prob M i a 0) :
    ∃ M' : CMP A, ModifiedLaw M M' α := 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, first display 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