Construct a one-block heat-bath update

AutoSamplingTheory.TechnicalLemmas.Probability.HeatBath.heatBathSnd · def · Teaching coverage

Statement

Under the product-space hypotheses, define a kernel Hμ from α × β back to α × β by first projecting the input to its first coordinate and then pairing the identity kernel on that coordinate with the selected conditional distribution of the second coordinate. This is a noncomputable law construction; it does not implement a procedure for drawing a conditional sample.

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.

Construction and meaning

noncomputable def heatBathSnd (μ : Measure (α × β)) [IsFiniteMeasure μ] :
    Kernel (α × β) (α × β)

noncomputable def heatBathSnd (μ : Measure (α × β)) [IsFiniteMeasure μ] :
    Kernel (α × β) (α × β) :=
  (Kernel.id ×ₖ condDistrib Prod.snd Prod.fst μ) ∘ₖ
    Kernel.deterministic Prod.fst measurable_fst

/-- The selected conditional distribution gives a Markov update at every state,
including states over first-marginal null fibers. This is a mass-one assertion,
not a conditional-support assertion on such fibers. -/

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.