Samplinglib mathematical lesson

The evolved-measure form of finite-step invariance

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

Read this first

Mathematical 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.\]

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.

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.

Download module (.lean)

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

Exact module and namespace context

Proof roadmap

1Reuse 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ⁿ.
2Read 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.

Full assumptions and notation

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 verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

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.

Download module (.lean)

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.

Sources, dependencies, and reuse

Source and reuse

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

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