The exact output law is a retained Dirac factor times a conditional law

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

Statement

For every input pair x under the finite-measure conditional-existence hypotheses, the measure returned by heatBathSnd μ at x is exactly the ordinary product of the Dirac measure at x's first coordinate and the selected conditional law of the second coordinate given that value. This is a pointwise identity for the chosen kernel, not pointwise uniqueness of conditional distributions.

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.
• (x : α × β) — An arbitrary input x=(a,b), with no positivity or support condition.

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

@[simp] theorem heatBathSnd_apply (μ : Measure (α × β)) [IsFiniteMeasure μ]
    (x : α × β) :
    heatBathSnd μ x = (Measure.dirac x.1).prod (condDistrib Prod.snd Prod.fst μ x.1)

@[simp] theorem heatBathSnd_apply (μ : Measure (α × β)) [IsFiniteMeasure μ]
    (x : α × β) :
    heatBathSnd μ x = (Measure.dirac x.1).prod (condDistrib Prod.snd Prod.fst μ x.1) := by
  rw [heatBathSnd, Kernel.comp_deterministic_eq_comap, Kernel.comap_apply,
    Kernel.prod_apply, Kernel.id_apply]

/-- A second-coordinate heat-bath update leaves its finite joint target invariant.

The zero measure is allowed. This theorem does not imply irreducibility,
reversibility, convergence from another initial law, or any mixing rate. -/

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.