Coordinate splitting and reconstruction preserve mass one

AutoSamplingTheory.TechnicalLemmas.Probability.CoordinateHeatBath.heatBath_isMarkovKernel · instance · Teaching coverage

Statement

For every finite target and fixed selected coordinate under the construction's exact hypotheses, the coordinate heat-bath update is a Markov kernel on the full dependent product. At every starting state x its output law has total mass one, regardless of the target mass or whether the retained fiber has positive target mass.

All objects and hypotheses

• {n : ℕ} — n is an arbitrary natural number, so Fin (n+1) is a nonempty finite index set. Individual coordinate spaces need not be finite.
• (X : Fin (n + 1) → Type*) — X is a possibly dependent family: coordinate j may have its own type X j. A state x is a function choosing x j : X j for every j.
• [∀ j, MeasurableSpace (X j)] — Each coordinate is measurable; the full and retained products use their product sigma-algebras.
• (μ : Measure (∀ j, X j)) [IsFiniteMeasure μ] — μ is any finite measure on the full state space. It may have zero mass or be unnormalized.
• (i : Fin (n + 1)) — i is a fixed selected coordinate, not a randomly drawn index.
• [StandardBorelSpace (X i)] [Nonempty (X i)] — Only the selected coordinate must be nonempty and Standard Borel. The other coordinates need neither condition for the construction, Markovness, or invariance.

Notation and interpretation

S

The dependent full state space, written ∀ j, X j in Lean.

\[S=\prod_{j\in\operatorname{Fin}(n+1)}X_j\]

R_i

The retained-coordinate product. i.succAbove lists every original index except i; k is its own Fin n index.

\[R_i=\prod_{k\in\operatorname{Fin}(n)}X_{i.\operatorname{succAbove}(k)}\]

r_i

The tuple of all unselected coordinates; this is explanatory notation, not a newly introduced Lean declaration.

\[r_i(x)(k)=x(i.\operatorname{succAbove}(k))\]

e_i

MeasurableEquiv.piFinSuccAbove X i first places Xi before Ri; composing with prodComm puts retained coordinates first. e_i and its inverse are measurable.

\[e_i:S\simeq_{\mathrm{meas}}R_i\times X_i,\qquad e_i(x)=(r_i(x),x_i)\]

η_i,m_i,q_i

Pushed-forward joint target, retained marginal, and selected conditional version.

\[\eta_i=(e_i)_\#\mu,\qquad m_i=(\operatorname{fst})_\#\eta_i,\qquad q_i(r)=\operatorname{condDistrib}(\operatorname{snd}\mid\operatorname{fst};\eta_i)(r)\]

K_i

The existing public CoordinateHeatBath.heatBath X μ i; this evaluated formula uses HeatBath.heatBathSnd_apply.

\[K_i(x)=(e_i^{-1})_\#\bigl(\delta_{r_i(x)}\otimes q_i(r_i(x))\bigr)\]

• All sets used to test equality of measures are measurable unless explicitly stated otherwise.
• All measure values, reciprocals and scalar multiplications in the Lean conditional formula are in ℝ≥0∞. Integral displays of kernel probabilities denote nonnegative extended integrals, not Bochner integrals with unstated integrability hypotheses.
• The notation r_i, F_i, e_i, q_i and K_i in the teaching text is explanatory mathematical shorthand, not new public Lean definitions.
• Markovness quantifies over every input; a selected conditional version's law characterization is only marginal-a.e. unless a positive-atom/fiber theorem applies.
• Finite target mass is not probability normalization. Fin (n+1) counts sites, not states. No law is assumed to have a density.

Mathematical proof

instance heatBath_isMarkovKernel (μ : Measure (∀ j, X j)) [IsFiniteMeasure μ]
    (i : Fin (n + 1)) [StandardBorelSpace (X i)] [Nonempty (X i)] :
    IsMarkovKernel (heatBath X μ i)

instance heatBath_isMarkovKernel (μ : Measure (∀ j, X j)) [IsFiniteMeasure μ]
    (i : Fin (n + 1)) [StandardBorelSpace (X i)] [Nonempty (X i)] :
    IsMarkovKernel (heatBath X μ i) := by
  unfold heatBath
  exact Kernel.IsMarkovKernel.map _
    ((MeasurableEquiv.piFinSuccAbove X i).trans MeasurableEquiv.prodComm).symm.measurable

/-- Exact invariance by literal reuse of one-block heat-bath and measurable
kernel transport. No convergence from other initial laws is inferred. -/

Scope and omitted-condition boundaries

• These are existing source-neutral measure/kernel interfaces, not newly proved claims in this research packet. Reading source and historical tests is not a fresh Lean build or independent verification.
• Finite target measure means μ(univ) < ∞, not μ(univ) = 1; zero and finite unnormalized targets are allowed unless a positive-fiber hypothesis rules them out.
• A selected regular conditional distribution is a probability kernel at every conditioning value. Its conditional-law characterization is determined only almost everywhere under the conditioning marginal; null fibers have no asserted feasible/Gibbs-support property.
• No reversibility, irreducibility, ergodicity, convergence from a different initial law, mixing rate, random scan, scan-order correctness, executable conditional sampling or cost bound follows from these declarations alone.