Prove2Me

Proposition C.2.3 — a cost drift condition (C.14) bounds ciGc_{iG} by r(i)+FmiGr(i) + F m_{iG}

Proved
SennottDP.MarkovCost.lyapunov_passage_cost_bound

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). Let G⊆SG \subseteq S be nonempty with miG<∞m_{iG} < \infty for all i∉Gi \notin G. Suppose there are a finite nonnegative function rr on SS and a finite set H⊆S−GH \subseteq S - G with

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

Then there is a finite nonnegative constant FF such that

ciG≤r(i)+F miG,i∉G.c_{iG} \le r(i) + F\, m_{iG}, \qquad i \notin G.

If H=∅H = \emptyset, then ciG≤r(i)c_{iG} \le r(i) for i∉Gi \notin G.

This is the Lyapunov criterion for finiteness of expected first passage costs.

Formalization Note Because rr is finite, the first condition of (C.14) is written ∑jPij r(j)+C(i)≤r(i)\sum_j P_{ij}\, r(j) + C(i) \le r(i) in [0,∞][0,\infty]. HH is a Finset disjoint from GG; FF is an ℝ≥0 constant chosen before ii.

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), Proposition C.2.3, p. 300. Let `G` be a nonempty subset of `S` with
`m_{iG} < ∞` for all `i ∉ G`. Let `r` be a finite nonnegative function on `S` and `H ⊆ S − G` a
finite set with (C.14): `∑_j P_{ij}[r(j) − r(i)] ≤ −C(i)` for `i ∉ G ∪ H` (written
`∑_j P_{ij} r(j) + C(i) ≤ r(i)`) and `∑_j P_{ij} r(j) < ∞` for `i ∈ H`. Then there is a finite
nonnegative constant `F` with `c_{iG} ≤ r(i) + F m_{iG}` for `i ∉ G`; if `H = ∅`, then
`c_{iG} ≤ r(i)` for `i ∉ G`. -/
theorem lyapunov_passage_cost_bound {S : Type} [Countable S] (M : MC S) (C : S → ℝ≥0)
    (G : Set S) (hG : G.Nonempty) (hm : ∀ i ∉ G, meanPassage M G i < ⊤)
    (r : S → ℝ≥0) (H : Finset S) (hHG : Disjoint (H : Set S) G)
    (hdrift : ∀ i ∉ G, i ∉ H → ∑' j, M.P i j * (r j : ℝ≥0∞) + C i ≤ r i)
    (hH : ∀ i ∈ H, ∑' j, M.P i j * (r j : ℝ≥0∞) < ⊤) :
    (∃ F : ℝ≥0, ∀ i ∉ G, passageCost M C G i ≤ r i + F * meanPassage M G i) ∧
    (H = ∅ → ∀ i ∉ G, passageCost M C G i ≤ r i) := by sorry

end SennottDP.MarkovCost
Source
Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999), p. 300, Proposition C.2.3, Eq. (C.14)
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