The coordinate update preserves the original finite target

AutoSamplingTheory.TechnicalLemmas.Probability.CoordinateHeatBath.heatBath_invariant · theorem · Teaching coverage

Statement

For every finite measure μ on the dependent coordinate product, a fixed selected coordinate's heat-bath kernel preserves μ, provided only that all coordinates are measurable and the selected coordinate is nonempty Standard Borel. No singleton-measurability, density, positive-support, or probability-normalization assumption is used.

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

theorem heatBath_invariant (μ : Measure (∀ j, X j)) [IsFiniteMeasure μ]
    (i : Fin (n + 1)) [StandardBorelSpace (X i)] [Nonempty (X i)] :
    (heatBath X μ i).Invariant μ

theorem heatBath_invariant (μ : Measure (∀ j, X j)) [IsFiniteMeasure μ]
    (i : Fin (n + 1)) [StandardBorelSpace (X i)] [Nonempty (X i)] :
    (heatBath X μ i).Invariant μ := by
  let e := (MeasurableEquiv.piFinSuccAbove X i).trans MeasurableEquiv.prodComm
  simpa only [heatBath, MeasurableEquiv.symm_symm, MeasurableEquiv.map_symm_map] using
    KernelTransport.invariant_map_comap e.symm (HeatBath.heatBathSnd_invariant (μ.map e))

/-- At each input `x`, every coordinate other than the selected one is retained
almost surely. Singleton measurability is needed only at the retained coordinate
`j`: equality of a marginal law with a Dirac measure on a coarse measurable
space would not alone imply literal almost-everywhere equality. -/

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.