Lemma 2.2.1 — the ergodic lemma behind Loynes' theorem

Proved

PalmQueueing.Loynes.ergodic_lemma

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

palm-calculusqueueingstabilitystationary-process

Lemma 2.2.1. Let $Z$ be non-negative, $P^0$ -a.s. finite, and such that $Z - Z \circ \theta \in L^1(P^0)$ . Then $E^0[Z - Z\circ\theta] = 0$ .

The book's proof is three lines: for any $C > 0$ , $|Z \wedge C - (Z \wedge C)\circ\theta| \le |Z - Z\circ\theta|$ , and the conclusion follows from $E^0[Z \wedge C - (Z\wedge C)\circ\theta] = 0$ and dominated convergence.

It is the lemma the uniqueness half of Loynes' theorem runs on. Applied to a finite solution $Z$ of (2.2.1), for which $Z\circ\theta - Z \le \sigma$ and $Z\circ\theta - Z \ge \sigma - \tau$ (2.2.15), it gives $E^0[Z\circ\theta - Z] = 0$ ; applied to the difference of two stationary solutions it forces that difference to be $\theta$ -invariant, and ergodicity then forces it to be constant.

$Z$ being real-valued, " $P^0$ -a.s. finite" is carried by the type. The hypothesis that is not automatic and is what the lemma actually needs is the $\theta$ -invariance of $P^0$ , which Eq. (1.2.16) of Chapter 1 supplies for the point shift.

Preamble

import Mathlib

/-!
# Lemma 2.2.1: the ergodic lemma behind Loynes' theorem (§2.2.3, p.87)
-/

Formal statement

namespace PalmQueueing.Loynes

open MeasureTheory

variable {Ω : Type*} [MeasurableSpace Ω]

/-- **Lemma 2.2.1** (p.87). Let `Z` be non-negative, `P⁰`-a.s. finite, and such that
`Z − Z ∘ θ ∈ L¹(P⁰)`. Then `E⁰[Z − Z ∘ θ] = 0`.

The lemma is what makes the uniqueness half of Loynes' theorem work: applied to the difference of
two stationary solutions it forces that difference to be constant, and the flow's ergodicity then
forces it to be zero. The book's own proof is three lines — for any `C > 0`,
`|Z ∧ C − (Z ∧ C) ∘ θ| ≤ |Z − Z ∘ θ|`, and the conclusion follows from
`E⁰[Z ∧ C − (Z ∧ C) ∘ θ] = 0` and dominated convergence.

`Z` is `ℝ`-valued, so "`P⁰`-a.s. finite" is carried by the type. The hypothesis that matters and is
not automatic is the `θ`-invariance of `P⁰`, which Chapter 1's Eq. (1.2.16) supplies. -/
theorem ergodic_lemma (P0 : Measure Ω) [IsProbabilityMeasure P0]
    (shift : Ω → Ω) (hshift : Measurable shift) (hinv : Measure.map shift P0 = P0)
    (Z : Ω → ℝ) (hZmeas : Measurable Z) (hZ0 : ∀ ω, 0 ≤ Z ω)
    (hint : Integrable (fun ω => Z ω - Z (shift ω)) P0) :
    ∫ ω, (Z ω - Z (shift ω)) ∂P0 = 0 := by sorry

end PalmQueueing.Loynes

Source

Baccelli & Bremaud, Elements of Queueing Theory: Palm Martingale Calculus and Stochastic Recurrences, 2nd ed., Springer 2003, p. 87, Lemma 2.2.1

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