KernelInvariance: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

An invariant measure remains invariant after any finite number of transitions
The evolved-measure form of finite-step invariance

ASTIS mathematical exposition

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.

\[\mu K=\mu\quad\Longrightarrow\quad \forall n\in\mathbb N,\ \mu K^n=\mu.\qquad\text{Equivalently, }\int_A K^n(a,E)\,\mu(da)=\mu(E)\quad(E\text{ measurable}).\]

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

1. Zero transitions do nothing

Prove the claim by induction on n. At n=0, the power is the identity kernel, which sends every input a to the point mass δₐ. Applying this kernel simply returns the original measure, so the base case is true.

\[\mu K^0=\mu I=\mu,\qquad I(a,\cdot)=\delta_a.\]

Corresponding Lean step

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

Measure.id_comp is the identity bind law; no assumption that μ has total mass one is used.

2. Append one transition and reassociate

Assume μKⁿ=μ. The successor power is Kⁿ∘ₖK, where the rightmost K is applied first. Associativity of composing measures and kernels says that starting from μ and applying this composite is the same as first evolving μ by K and then by Kⁿ.

\[\mu K^{n+1}=\mu(K^n\circ_{\!k}K)=(\mu K)K^n.\]

Corresponding Lean step

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

The proof uses this associativity through ProbabilityTheory.Kernel.Invariant.comp in the next line; it does not call Chapman–Kolmogorov as a separate theorem.

3. Use one-step invariance and the induction hypothesis

The first transition returns μ by the supplied assumption, and the remaining n transitions return μ by the induction hypothesis. Hence the successor case holds. Together with the base case, induction proves the assertion for every natural n.

\[(\mu K)K^n=\mu K^n=\mu.\]

Corresponding Lean step

exact ih.comp hκ

ih supplies invariance of κⁿ, hκ supplies invariance of κ; Invariant.comp returns invariance of κⁿ∘ₖκ in precisely this order.

Lean statement · invariant_pow

Braces mark inputs Lean usually infers; square brackets ask it to find the measurable-space structure. Kernel α α is a measurable family of measures, not automatically a Markov kernel. hκ is a proof of the input equality μ.bind κ = μ. The explicit n may be any natural number. The expression after the final colon is the proposition to be proved: μ is invariant for the power κ^n.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

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

Exact module and namespace context

Lean proof · invariant_pow

The two induction branches correspond exactly to zero transitions and one-more-than-n transitions. ih is the already-established invariance of κ^n. The final line applies the existing composition theorem to ih and hκ; it is a mathematical closure argument, not a test or simulation.

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. -/

Exact module and namespace context

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.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

ProbabilityTheory.Kernel.Invariant
ProbabilityTheory.Kernel.Invariant.comp
MeasureTheory.Measure.id_comp
ProbabilityTheory.Kernel.id
pow_succ

MeasureTheory.Measure.comp_assoc: Inside the inspected implementation of Invariant.comp, not a separately written call in invariant_pow.

ProbabilityTheory.Kernel.pow_add: Available from the imported kernel-power API, but not called by this proof; do not draw it as a direct proof dependency.

Mathematical sources

ASTIS statement and proof — Directly inspected local theorem.
Mathlib invariant-composition identity — Direct mathematical dependency.
Mathlib identity kernel acting on a measure — Direct base-case dependency.
Module card — Local explanation of assumptions and reuse; not a primary textbook citation.
Focused tests (consumer evidence) — First test specializes invariant_pow to n=7 without Markovness. Second obtains invariance from supplied reversibility using ProbabilityTheory.Kernel.IsReversible.invariant under an explicit IsMarkovKernel hypothesis, then calls bind_pow_eq at n=5. The Markov hypothesis belongs to reversibility→invariance, not invariant_pow.

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

ASTIS mathematical exposition

The evolved-measure form of finite-step invariance

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

Statement

On an arbitrary measurable space A, let K:A→𝓜(A) be a kernel, μ a measure, and suppose μK=μ. For each natural n, binding μ to Kⁿ gives exactly μ. This is the same finite-step invariance result written as an equality of measures instead of the predicate Invariant; it introduces no additional mathematical conclusion.

\[\mu.\operatorname{bind}(K^n)=\mu,\qquad\text{that is, }\mu K^n=\mu.\]

All objects and hypotheses

α : Type* with [MeasurableSpace α].
κ : Kernel α α and μ : Measure α; neither finiteness nor Markovness is assumed.
hκ : κ.Invariant μ.
n : ℕ. No omitted section variables or extra hypotheses.

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

1. Reuse the finite-iteration theorem

Apply invariant_pow to the one-step invariance assumption and the chosen n. This already proves that μ is invariant for Kⁿ.

\[\operatorname{Invariant}(K,\mu)\Longrightarrow\operatorname{Invariant}(K^n,\mu).\]

Corresponding Lean step

invariant_pow hκ n

2. Read the predicate as its defining equality

By definition, a measure is invariant for a kernel precisely when binding it to that kernel leaves it unchanged. Exposing that definition gives the requested equality, without any new induction or integral argument.

\[\operatorname{Invariant}(K^n,\mu)\ \equiv\ \mu.\operatorname{bind}(K^n)=\mu.\]

Corresponding Lean step

(invariant_pow hκ n).def

Lean statement · bind_pow_eq

μ.bind (κ ^ n) is Lean's measure obtained by applying the n-step kernel to μ. The type annotation distinguishes this equality from equality of kernels or densities. Inputs and assumptions are exactly those of invariant_pow.

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

Exact module and namespace context

Lean proof · bind_pow_eq

The expression invariant_pow hκ n supplies a proof of (κ^n).Invariant μ. Its .def projection is the Mathlib theorem that exposes the equality stored in the invariant predicate. This declaration exists for convenient measure-level rewriting, not as a second independent mathematical leaf.

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

end KernelInvariance
end Probability
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

Scope and omitted-condition boundaries

Same mathematical boundary as invariant_pow; count this as a reuse/notation wrapper, not a new stationary-distribution or mixing theorem.
A downstream reversible-kernel use still needs the Markov assumption required by Mathlib IsReversible.invariant before this wrapper can be applied.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Probability.KernelInvariance.invariant_pow

Mathlib API called (external library)

ProbabilityTheory.Kernel.Invariant
MeasureTheory.Measure.bind

Mathematical sources

ASTIS measure-level wrapper — Directly inspected wrapper.
Definition-exposure theorem — Exact meaning of .def.
Focused tests (consumer evidence) — First test specializes invariant_pow to n=7 without Markovness. Second obtains invariance from supplied reversibility using ProbabilityTheory.Kernel.IsReversible.invariant under an explicit IsMarkovKernel hypothesis, then calls bind_pow_eq at n=5. The Markov hypothesis belongs to reversibility→invariance, not invariant_pow.

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.