Every one-block update is a probability law

AutoSamplingTheory.TechnicalLemmas.Probability.HeatBath.heatBathSnd_isMarkovKernel · instance · Teaching coverage

Statement

For every finite joint μ under the stated coordinate hypotheses, heatBathSnd μ is a Markov kernel: for every input x, its output measure has total mass one. This remains true if μ is zero or x lies over a first-marginal-null conditioning value.

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

instance heatBathSnd_isMarkovKernel (μ : Measure (α × β)) [IsFiniteMeasure μ] :
    IsMarkovKernel (heatBathSnd μ)

instance heatBathSnd_isMarkovKernel (μ : Measure (α × β)) [IsFiniteMeasure μ] :
    IsMarkovKernel (heatBathSnd μ) := by
  unfold heatBathSnd
  infer_instance

/-- Pointwise product-law form of the update, using the selected conditional
version. The Dirac factor retains the first coordinate. -/

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.