HeatBath: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

Construct a one-block heat-bath update
Every one-block update is a probability law
The exact output law is a retained Dirac factor times a conditional law
A one-block heat-bath step preserves the finite joint target

ASTIS mathematical exposition

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.

\[H_\mu=(\operatorname{Id}_\alpha\times_k q)\circ_k D_{\operatorname{fst}},\qquad D_{\operatorname{fst}}(a,b)=\delta_a.\]

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

1. Forget only the old resampled value

The deterministic first-projection kernel turns (a,b) into the point-mass law at a. Its measurability is supplied by the measurable first projection. This determines which information the update retains.

\[(a,b)\xrightarrow{D_{\operatorname{fst}}}\delta_a.\]

Corresponding Lean step

Kernel.deterministic Prod.fst measurable_fst.

2. Build a joint output law at a retained value

At a, Kernel.id gives δa and condDistrib Prod.snd Prod.fst μ gives q(a). Their kernel product is a measurable family of laws on α × β. The conditional kernel comes from the finite-measure disintegration machinery, with β nonempty and Standard Borel.

\[(\operatorname{Id}_\alpha\times_k q)(a)=\delta_a\otimes q(a).\]

Corresponding Lean step

Kernel.id ×ₖ condDistrib Prod.snd Prod.fst μ. The pointwise evaluation is separately proved by heatBathSnd_apply.

3. Compose in the order of the experiment

Compose the output-law kernel after the deterministic projection, obtaining a state-to-state kernel. In κ ∘ₖ η, η acts first. The old second coordinate is not used in selecting q(a). The following theorems establish its mass-one and invariant-law properties; these are not additional clauses of the definition.

\[\alpha\times\beta\xrightarrow{D_{\operatorname{fst}}}\alpha\xrightarrow{\operatorname{Id}_\alpha\times_k q}\alpha\times\beta.\]

Corresponding Lean step

The definition is the displayed composition. noncomputable records that the conditional version is selected nonconstructively.

Lean statement · heatBathSnd

Keep a, redraw b from the selected law conditioned on a, and regard the result as a law for the whole pair. The word noncomputable warns that an abstract conditional distribution need not come with a usable sampling algorithm.

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.

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

Exact module and namespace context

Lean construction · heatBathSnd

`Kernel (α × β) (α × β)` means a measurable assignment from each input state to an output measure. `Kernel.id` is the probabilistic identity kernel a ↦ δa, not an ordinary function that returns a directly. `×ₖ` forms a product of two kernels with the same input; it returns a law on the pair of output spaces. `∘ₖ` composes kernels in right-to-left order. `measurable_fst` is an actual measurability proof, not a placeholder.

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

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.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

ProbabilityTheory.Kernel.id
ProbabilityTheory.condDistrib
ProbabilityTheory.Kernel.prod
ProbabilityTheory.Kernel.comp
ProbabilityTheory.Kernel.deterministic
measurable_fst

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 — 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) — The definition is exercised by its Markovness, product-law, invariance, finite-power and zero-target consumers.

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.

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

ASTIS mathematical exposition

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.

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

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

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

Exact module and namespace context

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.

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

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.

Source and reuse

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

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

ASTIS mathematical exposition

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.

\[H_\mu(x)=\delta_{x_1}\otimes q(x_1)\qquad(x\in\alpha\times\beta).\]

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

1. Replace deterministic precomposition by input substitution

Composing a kernel with a deterministic map evaluates that kernel at the mapped input. The identity is between kernels and does not require a singleton-measurable retained space.

\[(L\circ_k D_f)(x)=L(f(x)),\qquad f=\operatorname{fst}.\]

Corresponding Lean step

Kernel.comp_deterministic_eq_comap turns the composition into a comap; Kernel.comap_apply evaluates the comap.

2. Evaluate the product kernel

The product kernel evaluated at x1 is the product of its two measure values at x1. Markovness supplies the s-finiteness needed by the kernel-product evaluation machinery.

\[(\operatorname{Id}_\alpha\times_k q)(x_1)=\operatorname{Id}_\alpha(x_1)\otimes q(x_1).\]

Corresponding Lean step

Kernel.prod_apply.

3. Evaluate the identity kernel

The identity kernel returns the Dirac measure at its input. Substituting this gives the desired measure identity. The x2 component never enters the expression.

\[\operatorname{Id}_\alpha(x_1)=\delta_{x_1},\qquad H_\mu(x)=\delta_{x_1}\otimes q(x_1).\]

Corresponding Lean step

Kernel.id_apply completes the rw chain.

Lean statement · heatBathSnd_apply

Once a starting pair is fixed, the update's whole law can be written down compactly: a point mass on the retained coordinate, multiplied by the conditional law on the updated coordinate. The equality is valid even at a null conditioning value because it refers to the version already selected.

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

Exact module and namespace context

Lean proof · heatBathSnd_apply

`@[simp]` marks the proven equality as a standard simplification rule for later uses; it does not weaken the statement. `rw [heatBathSnd, ...]` performs a sequence of equality rewrites, each corresponding to one of the evaluation steps. `x.1` means the first projection of x. `Measure.prod` is a product of two measures, whereas the construction used the product `×ₖ` of two kernels. Equality of this retained marginal law with a Dirac measure is not automatically literal almost-everywhere equality of retained values on an arbitrary coarse sigma-algebra; the coordinate-retention theorem makes its singleton assumption explicit.

@[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. -/

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.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Probability.HeatBath.heatBathSnd

Mathlib API called (external library)

ProbabilityTheory.Kernel.comp_deterministic_eq_comap
ProbabilityTheory.Kernel.comap_apply
ProbabilityTheory.Kernel.prod_apply
ProbabilityTheory.Kernel.id_apply

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_apply — 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) — An example consumes exactly this pointwise equality for arbitrary x.

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

ASTIS mathematical exposition

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.

\[H_\mu\circ_m\mu=\mu,\qquad\text{equivalently }\int_{\alpha\times\beta}H_\mu(x,A)\,\mu(dx)=\mu(A)\ \text{for every measurable }A.\]

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. Unpack invariance and regroup the two stages

Let L be the product kernel retaining the first coordinate and drawing the second from its conditional law, and let D be the deterministic first-projection kernel. Acting with their composite on μ is the same as first acting with D and then L. This reassociation is a measure/kernel composition identity; it does not require an additional s-finiteness premise.

\[H_\mu\circ_m\mu=(L\circ_k D)\circ_m\mu=L\circ_m(D\circ_m\mu).\]

Corresponding Lean step

change exposes the definition of Kernel.Invariant and of heatBathSnd; ← Measure.comp_assoc reassociates.

2. The deterministic first stage produces the first marginal

A deterministic kernel acts on a measure by pushforward along its function. For the first projection this is exactly m.

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

Corresponding Lean step

Measure.deterministic_comp_eq_map.

3. Recognize reconstruction as a composition-product

Applying a kernel whose output at a is the pair of the retained Dirac value and q(a) to m produces the joint measure m ⊗ₘ q. This is why the retained identity factor was included in the construction. This step uses Measure.compProd_eq_comp_prod, whose hypotheses require an s-finite first marginal and an s-finite conditional kernel. Here the marginal is finite and the conditional kernel is Markov, so both instances are available.

\[(\operatorname{Id}_\alpha\times_k q)\circ_m m=m\otimes_m q.\]

Corresponding Lean step

← Measure.compProd_eq_comp_prod.

4. Reuse the joint-law identity

The conditional-resampling theorem already proves that this composition-product recovers μ. Combining the three equalities establishes invariance without any density computation or acceptance-ratio argument.

\[H_\mu\circ_m\mu=m\otimes_m q=\mu.\]

Corresponding Lean step

exact ConditionalResampling.fst_compProd_condDistrib_snd_eq_self.

Lean statement · heatBathSnd_invariant

If a pair already has the target joint distribution, keeping its first coordinate preserves the correct first marginal. Redrawing the second coordinate from the correct conditional law then reconstructs that same joint distribution. This is stationarity, not a convergence guarantee.

theorem heatBathSnd_invariant (μ : Measure (α × β)) [IsFiniteMeasure μ] :
    (heatBathSnd μ).Invariant μ

Exact module and namespace context

Lean proof · heatBathSnd_invariant

`Invariant μ` is a predicate on a kernel, meaning equality between the post-update measure and μ. `change` unfolds that target into a usable equation. The backward arrows in the rewrite list mean an existing equality is used from right to left, to reveal the marginal and composition-product forms. `exact` finishes with the earlier ASTIS theorem after the goal has become exactly its statement. The proof concerns the initial measure μ itself. It does not show that repeatedly updating an arbitrary initial distribution approaches μ.

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

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.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

ProbabilityTheory.Kernel.Invariant
MeasureTheory.Measure.comp_assoc
MeasureTheory.Measure.deterministic_comp_eq_map
MeasureTheory.Measure.compProd_eq_comp_prod

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_invariant — 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) — Tests direct invariance, zero-target invariance, and finite-power invariance using existing KernelInvariance.invariant_pow. That power theorem is a consumer, not a proof parent here.

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