A one-block heat-bath step preserves the finite joint target

AutoSamplingTheory.TechnicalLemmas.Probability.HeatBath.heatBathSnd_invariant · theorem · Teaching coverage

Statement

For every finite μ on α × β, with α measurable and β nonempty Standard Borel, heatBathSnd μ leaves μ invariant. Starting with measure μ and applying one update gives exactly μ again. This remains true for the zero measure and for finite targets that are not probability measures.

All objects and hypotheses

• {α β : Type*} — Two possibly universe-polymorphic coordinate types α and β.
• [MeasurableSpace α] [MeasurableSpace β] — Both carry measurable-space structures; α × β has the product sigma-algebra.
• [StandardBorelSpace β] — The resampled space β is Standard Borel, supplying the regular-conditional-distribution existence contract.
• [Nonempty β] — β is nonempty, so the selected conditional kernel can be totalized as a probability law even on marginal-null fibers.
• (μ : Measure (α × β)) [IsFiniteMeasure μ] — μ is any finite joint measure. It need not be normalized and may be zero. α need not be Standard Borel or nonempty.

Notation and interpretation

m

The first marginal, represented by μ.map Prod.fst.

\[m=(\operatorname{fst})_\#\mu\]

q

The particular regular conditional probability kernel selected by Mathlib, not a pointwise unique conditional density.

\[q(a)=\operatorname{condDistrib}(\operatorname{snd}\mid\operatorname{fst};\mu)(a)\]

μ ⊗ₘ q

Composition-product of a measure and a kernel, for measurable A ⊆ α × β. It is a joint measure, unlike ordinary kernel composition which forgets the intermediate state.

\[(m\otimes_m q)(A)=\int_\alpha q(a,\{b:(a,b)\in A\})\,m(da)\]

K ∘ₘ μ

The measure after one kernel application. Invariant means exactly K ∘ₘ μ = μ.

\[(K\circ_m\mu)(A)=\int K(x,A)\,\mu(dx)\]

• 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 heatBathSnd_invariant (μ : Measure (α × β)) [IsFiniteMeasure μ] :
    (heatBathSnd μ).Invariant μ

theorem heatBathSnd_invariant (μ : Measure (α × β)) [IsFiniteMeasure μ] :
    (heatBathSnd μ).Invariant μ := by
  change ((Kernel.id ×ₖ condDistrib Prod.snd Prod.fst μ) ∘ₖ
    Kernel.deterministic Prod.fst measurable_fst) ∘ₘ μ = μ
  rw [← Measure.comp_assoc, Measure.deterministic_comp_eq_map,
    ← Measure.compProd_eq_comp_prod]
  exact ConditionalResampling.fst_compProd_condDistrib_snd_eq_self

end AutoSamplingTheory.TechnicalLemmas.Probability.HeatBath

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.