Prove2Me

Corollary C.2.4 — the drift condition (C.16) gives ciz≤r(i)+Fmizc_{iz} \le r(i) + F m_{iz} and czz<∞c_{zz} < \infty

Proved
SennottDP.MarkovCost.lyapunov_return_cost_finite

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

average-costlyapunov-functionmarkov-chainp2o-batch-b23ap2o-gran-per-chapterp2o-plan-bookp2o-v1

Let Γ\Gamma be a Markov chain on a countable state space SS with finite nonnegative costs C(i)C(i), and let zz be a distinguished state with miz<∞m_{iz} < \infty for all ii. Suppose there are a finite nonnegative function rr on SS and a finite set H∗H^* containing zz with

∑jPij r(j)<∞,i∈H∗,∑jPij [r(j)−r(i)]≤−C(i),i∉H∗.(C.16)\sum_j P_{ij}\, r(j) < \infty, \quad i \in H^*, \qquad \sum_j P_{ij}\,[r(j) - r(i)] \le -C(i), \quad i \notin H^*. \tag{C.16}

Then there is a finite nonnegative constant FF such that ciz≤r(i)+F mizc_{iz} \le r(i) + F\, m_{iz} for i≠zi \ne z. If H∗={z}H^* = \{z\}, then ciz≤r(i)c_{iz} \le r(i) for i≠zi \ne z. Finally czz<∞c_{zz} < \infty.

Together with Corollary C.1.6 this gives a verifiable criterion for a chain to be zz standard.

Formalization Note The second condition of (C.16) is written ∑jPij r(j)+C(i)≤r(i)\sum_j P_{ij}\, r(j) + C(i) \le r(i) in [0,∞][0,\infty], equivalent since rr is finite; H∗H^* is a Finset.

Preamble
import Mathlib
import Definitions.Def_SennottDP_MarkovCost_Chain
import Definitions.Def_SennottDP_MarkovCost_Costs

open scoped ENNReal NNReal
open Filter Topology
Formal statement
namespace SennottDP.MarkovCost

/-- Sennott (1999), Corollary C.2.4, pp. 300–301. Assume `m_{iz} < ∞` for a distinguished state
`z` and all `i`. Let `r` be a finite nonnegative function on `S` and `H*` a finite set containing
`z` with (C.16): `∑_j P_{ij} r(j) < ∞` for `i ∈ H*` and `∑_j P_{ij}[r(j) − r(i)] ≤ −C(i)` for
`i ∉ H*` (written `∑_j P_{ij} r(j) + C(i) ≤ r(i)`). Then there is a finite nonnegative constant
`F` with `c_{iz} ≤ r(i) + F m_{iz}` for `i ≠ z`; if `H* = {z}`, then `c_{iz} ≤ r(i)` for `i ≠ z`;
finally `c_{zz} < ∞`. -/
theorem lyapunov_return_cost_finite {S : Type} [Countable S] (M : MC S) (C : S → ℝ≥0) (z : S)
    (hm : ∀ i, meanPassage M {z} i < ⊤) (r : S → ℝ≥0) (Hs : Finset S) (hzH : z ∈ Hs)
    (hH : ∀ i ∈ Hs, ∑' j, M.P i j * (r j : ℝ≥0∞) < ⊤)
    (hdrift : ∀ i ∉ Hs, ∑' j, M.P i j * (r j : ℝ≥0∞) + C i ≤ r i) :
    (∃ F : ℝ≥0, ∀ i, i ≠ z → passageCost M C {z} i ≤ r i + F * meanPassage M {z} i) ∧
    (Hs = {z} → ∀ i, i ≠ z → passageCost M C {z} i ≤ r i) ∧
    passageCost M C {z} z < ⊤ := by sorry

end SennottDP.MarkovCost
Source
Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999), pp. 300–301, Corollary C.2.4, Eq. (C.16)
Human review

  • Endorsed by Shuze Chen · Oct 2, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 2, 2026

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

View graph