Invariant measures survive a measurable change of coordinates

AutoSamplingTheory.TechnicalLemmas.Probability.KernelTransport.invariant_map_comap · theorem · Teaching coverage

Statement

Let A and B be arbitrary measurable spaces, e:A→B a measurable bijection with measurable inverse, K:A→𝓜(A) a kernel, and μ any measure on A preserved by K. Define the transported kernel Kᵉ on B by returning an input y to e⁻¹(y), applying K there, and pushing the output measure forward by e. Then Kᵉ preserves the pushforward measure e_*μ. No Markovness, finiteness, s-finiteness, topology, Standard-Borel or nonempty-space assumptions are needed.

All objects and hypotheses

• {α β : Type*}, [MeasurableSpace α], [MeasurableSpace β].
• κ : Kernel α α, with no Markov or s-finite-kernel hypothesis.
• μ : Measure α, with no finite, s-finite, nonzero or probability-measure hypothesis.
• e : α ≃ᵐ β: an actual bijective equivalence with measurable forward and inverse maps, not just a measurable map or an almost-everywhere inverse.
• hκ : κ.Invariant μ.
• No additional local section variables. The conclusion concerns measures/laws, not densities relative to a fixed reference measure.

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

change ((κ.comap e.symm e.symm.measurable).map e) ∘ₘ μ.map e = μ.map e
rw [← Measure.map_comp _ _ e.measurable,

theorem invariant_map_comap {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    {κ : Kernel α α} {μ : Measure α} (e : α ≃ᵐ β) (hκ : κ.Invariant μ) :
    ((κ.comap e.symm e.symm.measurable).map e).Invariant (μ.map e)

theorem invariant_map_comap {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    {κ : Kernel α α} {μ : Measure α} (e : α ≃ᵐ β) (hκ : κ.Invariant μ) :
    ((κ.comap e.symm e.symm.measurable).map e).Invariant (μ.map e) := by
  change ((κ.comap e.symm e.symm.measurable).map e) ∘ₘ μ.map e = μ.map e
  rw [← Measure.map_comp _ _ e.measurable,
    ← Kernel.comp_deterministic_eq_comap, ← Measure.comp_assoc,
    Measure.deterministic_comp_eq_map, e.map_symm_map, hκ.def]

end AutoSamplingTheory.TechnicalLemmas.Probability.KernelTransport

Scope and omitted-condition boundaries

• Transport requires an actual measurable equivalence. This theorem does not handle arbitrary noninvertible maps or merely almost-everywhere coordinate inverses.
• Measurability of e ensures Kernel.map uses its genuine pushforward branch, not its nonmeasurable zero fallback.
• This is exact invariance only: no reversibility, irreducibility, convergence, mixing, Jacobian/density formula, or computational-cost conclusion.
• No ASTIS HeatBath, KernelMixture or KernelInvariance declaration is a proof prerequisite; they occur only in concrete consumer tests.
• Coordinate heat-bath tests add finite joint target and nonempty Standard-Borel resampled-coordinate assumptions. Conditional representatives there remain marginal-almost-everywhere objects.
• Private test constructions are not public coordinate-update algorithms and do not establish general retained-coordinate behavior, concrete Gibbs support/normalization, or source-copy-index repair.
• Exact directly inspected proof source is Mathlib measure/kernel algebra. Textbook anchors in local provenance records are motivation, not independently checked numbered-source assimilation.