An invariant measure remains invariant after any finite number of transitions

AutoSamplingTheory.TechnicalLemmas.Probability.KernelInvariance.invariant_pow · theorem · Teaching coverage

Statement

Let A be an arbitrary measurable space, let K be a kernel from A to itself, and let μ be any measure on A. Suppose one transition leaves μ unchanged: μK=μ. Then, for every natural number n, applying the n-fold kernel Kⁿ also leaves μ unchanged. The case n=0 is included. When K is Markov and μ is a probability measure this says that a chain initialized in stationarity remains stationary at every finite time, but neither normalization is required for the actual theorem.

All objects and hypotheses

• α : Type* with [MeasurableSpace α]; no topology, nonempty or Standard-Borel assumption.
• κ : ProbabilityTheory.Kernel α α; no IsMarkovKernel or IsSFiniteKernel assumption.
• μ : MeasureTheory.Measure α; no finite, s-finite, nonzero or probability assumption.
• hκ : κ.Invariant μ, meaning μ.bind κ = μ.
• n : ℕ, including zero. No local section parameters beyond these.

Notation and interpretation

Measurable space and kernel

A measurable space is a set with a specified sigma-algebra of events. A kernel K from A to B assigns to each input a a measure K(a,·) on B, and a↦K(a,E) is measurable whenever E is measurable. A kernel need not assign probability measures unless Markovness is separately assumed.

\[K:A\to\mathcal M(B),\qquad a\mapsto K(a,E)\text{ measurable for every measurable }E\subseteq B.\]

Measure evolved by a kernel; invariance

Write μK for the measure obtained by starting with μ and applying K. Lean writes μ.bind K or K ∘ₘ μ. Invariance says that this evolved measure is exactly μ. If μ is a probability law this means a stationary initial distribution, but the definitions and these theorems also allow arbitrary measures.

\[(\mu K)(E)=\int_A K(a,E)\,\mu(da),\qquad \mu K=\mu.\]

Composition and powers

Lean's L ∘ₖ K applies K first and L second. The multiplicative identity is the identity kernel a↦δ_a, and powers are repeated composition. All integrals here are nonnegative extended-real (lower Lebesgue) integrals; no signed or Bochner integrability is silently assumed.

\[(L\circ_{\!k}K)(a,E)=\int L(b,E)\,K(a,db),\quad K^0(a,\cdot)=\delta_a,\quad K^{n+1}=K^n\circ_{\!k}K.\]

Markov and s-finite kernels

Markov means every output measure has total mass one. An s-finite kernel is a countable sum of finite kernels, where each finite kernel has a finite uniform bound on its total mass across inputs. Markovness supplies this s-finiteness automatically. S-finite is not the same hypothesis as sigma-finite, and is not merely a pointwise finiteness assertion.

\[K(a,B)=1\ \forall a\quad\text{(Markov)};\qquad K=\sum_{n=0}^{\infty}K_n,\quad \forall n\ \exists C_n<\infty\ \forall a,\ K_n(a,B)\le C_n\quad\text{(s-finite)}.\]

Nonnegative weights

ℝ≥0 consists of finite nonnegative real numbers; ℝ≥0∞ also allows infinity and is the codomain of measure values. The coercion wᵢ↦cᵢ puts finite weights into extended nonnegative arithmetic. Zero weights are permitted, including when component masses are infinite; this arithmetic uses 0·∞=0.

\[w_i\in[0,\infty),\qquad c_i=\iota(w_i)\in[0,\infty].\]

Measurable equivalence and pushforward

A measurable equivalence e is a bijection whose forward and inverse maps are both measurable. Its pushforward measure records the original mass of inverse images. This is transport of measures, not a density transformation with an implicit Jacobian.

\[(e_*\mu)(E)=\mu(e^{-1}(E)),\qquad (e^{-1})_*(e_*\mu)=\mu.\]

Mathematical proof

induction n with
| zero =>
    change Kernel.id.Invariant μ
    exact Measure.id_comp

| succ n ih =>
    rw [pow_succ]
    change ((κ ^ n) ∘ₖ κ).Invariant μ

theorem invariant_pow {α : Type*} [MeasurableSpace α]
    {κ : Kernel α α} {μ : Measure α}
    (hκ : κ.Invariant μ) (n : ℕ) :
    (κ ^ n).Invariant μ

theorem invariant_pow {α : Type*} [MeasurableSpace α]
    {κ : Kernel α α} {μ : Measure α}
    (hκ : κ.Invariant μ) (n : ℕ) :
    (κ ^ n).Invariant μ := by
  induction n with
  | zero =>
      change Kernel.id.Invariant μ
      exact Measure.id_comp
  | succ n ih =>
      rw [pow_succ]
      change ((κ ^ n) ∘ₖ κ).Invariant μ
      exact ih.comp hκ

/-- Measure-level form of `invariant_pow`: starting an invariant law and taking
`n` transitions leaves the law unchanged. -/

Scope and omitted-condition boundaries

• Starts from exactly μ; says nothing about another initial law approaching μ.
• No uniqueness, irreducibility, aperiodicity, reversibility, ergodicity, spectral gap, mixing rate, estimator error, or computational cost conclusion.
• Only finite natural-number iteration; no infinite-time limit is taken.
• No independently checked numbered textbook source anchor in this dossier; local provenance records are listed separately.