Samplinglib mathematical lesson

Every one-block update is a probability law

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

Read this first

Mathematical 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.

\[\forall x\in\alpha\times\beta,\qquad H_\mu(x,\alpha\times\beta)=1.\]

Lean statement · heatBathSnd_isMarkovKernel

A Markov update must return one whole probability distribution from every input. The target itself need not have mass one: it supplies relative conditional laws, while the transition from each input is still normalized.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

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

Exact module and namespace context

Proof roadmap

1Each component is Markov
The deterministic first projection and the identity kernel have Dirac output laws of total mass one. Mathlib's selected regular conditional distribution is also a probability kernel at every a, including otherwise undetermined marginal-null a.
2A product of probability laws has mass one
For each a, multiplying the two component masses shows that the product output is a probability measure. The existing kernel-product instance supplies this statement uniformly and measurably in a.
3Composition preserves mass one
The composed kernel integrates a constant total output mass of one against the deterministic probability input law. Its mass is therefore one. This is a statement about normalization only, not a formula for the chosen conditional measure on a null fiber.

Full assumptions and notation

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

1. Each component is Markov

The deterministic first projection and the identity kernel have Dirac output laws of total mass one. Mathlib's selected regular conditional distribution is also a probability kernel at every a, including otherwise undetermined marginal-null a.

\[D_{\operatorname{fst}}(x,\alpha)=1,\quad \operatorname{Id}_\alpha(a,\alpha)=1,\quad q(a,\beta)=1.\]

Corresponding Lean step

unfold heatBathSnd exposes the three components; their Markov instances are already in Mathlib.

2. A product of probability laws has mass one

For each a, multiplying the two component masses shows that the product output is a probability measure. The existing kernel-product instance supplies this statement uniformly and measurably in a.

\[(\delta_a\otimes q(a))(\alpha\times\beta)=\delta_a(\alpha)\,q(a,\beta)=1\cdot1=1.\]

Corresponding Lean step

ProbabilityTheory.Kernel.IsMarkovKernel.prod is found by infer_instance.

3. Composition preserves mass one

The composed kernel integrates a constant total output mass of one against the deterministic probability input law. Its mass is therefore one. This is a statement about normalization only, not a formula for the chosen conditional measure on a null fiber.

\[H_\mu(x,\alpha\times\beta)=\int_\alpha 1\,D_{\operatorname{fst}}(x,da)=1.\]

Corresponding Lean step

ProbabilityTheory.Kernel.IsMarkovKernel.comp and the deterministic instance close the goal through infer_instance.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof / instance · heatBathSnd_isMarkovKernel

`instance` registers a proved mathematical property for later automatic use; it does not assume that property. `unfold heatBathSnd` replaces the public name by its defining composition. `infer_instance` combines already proved facts that deterministic kernels, conditional kernels, products, and compositions are Markov. It is a short formal proof because the reusable closure theorems carry the work. The declaration has no parameter x because IsMarkovKernel contains a universal assertion over every input.

Download module (.lean)

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

Exact module and namespace context

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.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Probability.HeatBath.heatBathSnd

Mathlib API called (external library)

ProbabilityTheory.Kernel.IsMarkovKernel.prod
ProbabilityTheory.Kernel.IsMarkovKernel.comp
ProbabilityTheory.Kernel.isMarkovKernel_deterministic
ProbabilityTheory.condDistrib

Anonymous instances are identified by source anchors rather than guessed generated Lean names.

Mathematical sources

Fearnhead–Nemeth–Oates–Sherlock, arXiv:2407.12751v1, §2.1.1 Component-wise updates and Gibbs moves; printed page 48 / PDF page 54 — Conditional-update motivation only; the generic finite-measure regular-conditional-law contract is not a numbered-source theorem assimilation.
Chen–Štefankovič–Vigoda, arXiv:2307.13826v4, §1.3 Glauber dynamics/Gibbs sampler; printed/PDF page 5; support convention in §1.1 printed/PDF page 4 — Fixed-site update motivation, not full finite-binary-state algorithm or uniform-scan certification.
Existing ASTIS declaration AutoSamplingTheory.TechnicalLemmas.Probability.HeatBath.heatBathSnd_isMarkovKernel — Exact public declaration and proof/construction read from the local source. Line numbers are current source anchors; no new source certification or Lean build performed.
Focused tests (consumer evidence) — Includes IsMarkovKernel for arbitrary finite μ and for the zero target.

Older frontier cells and the coordinate card say the printed copy-index repair is pending. The later positive-fiber card and source-support audit record separate acceptance of the exact one-index correction as ASTIS-REPAIR-20260908-GlauberCopyIndex. The old PositiveFiberUpdate audit remains possible-source-error for its limited page-5 evidence window. Do not overwrite that history, call the original PDF corrected, call a null-fiber start a counterexample to the positive-support source convention, or infer full source fidelity. This packet reads local evidence only; it performs no new PDF/source certification.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.