CoordinateHeatBath: 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 heat-bath update at one coordinate
Coordinate splitting and reconstruction preserve mass one
The coordinate update preserves the original finite target
Every unselected coordinate stays unchanged almost surely

ASTIS mathematical exposition

Construct a heat-bath update at one coordinate

AutoSamplingTheory.TechnicalLemmas.Probability.CoordinateHeatBath.heatBath · def · Teaching coverage

Statement

For every finite target measure μ on a finite dependent product of measurable coordinate spaces and every selected index i whose coordinate type is nonempty Standard Borel, define heatBath X μ i by a measurable change of coordinates: retain all coordinates except i, resample coordinate i with the existing one-block heat-bath kernel for the transformed target, and map the output back to the original state space. No measurable-singleton assumptions are required for this construction.

\[K_i=\bigl(\operatorname{comap}_{e_i}H_{\eta_i}\bigr)\operatorname{.map}(e_i^{-1}),\qquad K_i(x)=(e_i^{-1})_\#H_{\eta_i}(e_i(x)).\]

All objects and hypotheses

{n : ℕ} — n is an arbitrary natural number, so Fin (n+1) is a nonempty finite index set. Individual coordinate spaces need not be finite.
(X : Fin (n + 1) → Type*) — X is a possibly dependent family: coordinate j may have its own type X j. A state x is a function choosing x j : X j for every j.
[∀ j, MeasurableSpace (X j)] — Each coordinate is measurable; the full and retained products use their product sigma-algebras.
(μ : Measure (∀ j, X j)) [IsFiniteMeasure μ] — μ is any finite measure on the full state space. It may have zero mass or be unnormalized.
(i : Fin (n + 1)) — i is a fixed selected coordinate, not a randomly drawn index.
[StandardBorelSpace (X i)] [Nonempty (X i)] — Only the selected coordinate must be nonempty and Standard Borel. The other coordinates need neither condition for the construction, Markovness, or invariance.

Notation and interpretation

S: The dependent full state space, written ∀ j, X j in Lean.
\[S=\prod_{j\in\operatorname{Fin}(n+1)}X_j\]
R_i: The retained-coordinate product. i.succAbove lists every original index except i; k is its own Fin n index.
\[R_i=\prod_{k\in\operatorname{Fin}(n)}X_{i.\operatorname{succAbove}(k)}\]
r_i: The tuple of all unselected coordinates; this is explanatory notation, not a newly introduced Lean declaration.
\[r_i(x)(k)=x(i.\operatorname{succAbove}(k))\]
e_i: MeasurableEquiv.piFinSuccAbove X i first places Xi before Ri; composing with prodComm puts retained coordinates first. e_i and its inverse are measurable.
\[e_i:S\simeq_{\mathrm{meas}}R_i\times X_i,\qquad e_i(x)=(r_i(x),x_i)\]
η_i,m_i,q_i: Pushed-forward joint target, retained marginal, and selected conditional version.
\[\eta_i=(e_i)_\#\mu,\qquad m_i=(\operatorname{fst})_\#\eta_i,\qquad q_i(r)=\operatorname{condDistrib}(\operatorname{snd}\mid\operatorname{fst};\eta_i)(r)\]
K_i: The existing public CoordinateHeatBath.heatBath X μ i; this evaluated formula uses HeatBath.heatBathSnd_apply.
\[K_i(x)=(e_i^{-1})_\#\bigl(\delta_{r_i(x)}\otimes q_i(r_i(x))\bigr)\]

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. Separate the selected coordinate from the retained tuple

Use Mathlib's measurable equivalence for inserting/removing one Fin-indexed coordinate. It initially returns (selected, retained); follow it by product commutation to return (retained, selected). No new proof of a splitting bijection is needed.

\[x\longmapsto(x_i,r_i(x))\longmapsto(r_i(x),x_i)=e_i(x).\]

Corresponding Lean step

let e := (MeasurableEquiv.piFinSuccAbove X i).trans MeasurableEquiv.prodComm.

2. Express the target in split coordinates

Push μ forward along e. The measure ηi is finite. Its second coordinate is Xi, exactly the space for which Standard Borel and nonempty instances are assumed, so the existing one-block construction can be applied to ηi.

\[\eta_i=(e_i)_\#\mu,\qquad H_{\eta_i}:R_i\times X_i\rightsquigarrow R_i\times X_i.\]

Corresponding Lean step

HeatBath.heatBathSnd (μ.map e); measurable equivalence and finite-measure map instances discharge the implicit requirements.

3. Move input and output in opposite directions

To update an original input x, use comap to evaluate the split-space kernel at e(x); then use map to push each output measure through e⁻¹. These are different operations: comap changes the input, map changes the output.

\[x\xmapsto{e_i}e_i(x)\xrightsquigarrow{H_{\eta_i}}\text{a split output}\xmapsto{e_i^{-1}}\text{an original-space output}.\]

Corresponding Lean step

((HeatBath.heatBathSnd (μ.map e)).comap e e.measurable).map e.symm.

4. Read the intended transition law without adding a new theorem

The existing one-block evaluation lemma identifies the split output measure as the retained Dirac law times the selected conditional law. The construction therefore has the explanatory formula below; the public source keeps only the single heatBath definition.

\[K_i(x)=(e_i^{-1})_\#\bigl(\delta_{r_i(x)}\otimes q_i(r_i(x))\bigr).\]

Corresponding Lean step

HeatBath.heatBathSnd_apply, Kernel.comap_apply and Kernel.map_apply explain evaluation; no additional public algorithm is introduced.

Lean statement · heatBath

Temporarily reorder the state into a pair: all coordinates being kept, followed by the one coordinate being updated. Apply the already understood pair update, then undo that reordering. This lets one general construction cover different types of coordinates.

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 heatBath (μ : Measure (∀ j, X j)) [IsFiniteMeasure μ]
    (i : Fin (n + 1)) [StandardBorelSpace (X i)] [Nonempty (X i)] :
    Kernel (∀ j, X j) (∀ j, X j)

Exact module and namespace context

Lean construction · heatBath

`∀ j, X j` is a dependent function type and represents one value at each coordinate. `Fin (n + 1)` records a finite nonempty set of coordinate indices, not a finite number of possible states. `e.symm` is the inverse measurable equivalence. `.comap e e.measurable` changes the input, and `.map e.symm` changes the output law. The definition is noncomputable because it inherits the selected regular conditional distribution. No claim about implementation or complexity is hidden in the construction.

noncomputable def heatBath (μ : Measure (∀ j, X j)) [IsFiniteMeasure μ]
    (i : Fin (n + 1)) [StandardBorelSpace (X i)] [Nonempty (X i)] :
    Kernel (∀ j, X j) (∀ j, X j) :=
  let e := (MeasurableEquiv.piFinSuccAbove X i).trans MeasurableEquiv.prodComm
  ((HeatBath.heatBathSnd (μ.map e)).comap e e.measurable).map e.symm

/-- The coordinate update has total mass one at every input. This does not
assert conditional support on marginal-null 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

AutoSamplingTheory.TechnicalLemmas.Probability.HeatBath.heatBathSnd

Mathlib API called (external library)

MeasurableEquiv.piFinSuccAbove
MeasurableEquiv.prodComm
MeasurableEquiv.trans
ProbabilityTheory.Kernel.comap
ProbabilityTheory.Kernel.map
MeasureTheory.Measure.map

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.CoordinateHeatBath.heatBath — 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.
.lake/packages/mathlib/Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean:569 — Existing imported proof/construction source, not a newly proved ASTIS theorem.
Focused tests (consumer evidence) — Exercises nonconstant three-site Boolean updates, zero targets, a retained coordinate with indiscrete sigma-algebra, and mixture/power consumers. No new tests run.

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

Coordinate splitting and reconstruction preserve mass one

AutoSamplingTheory.TechnicalLemmas.Probability.CoordinateHeatBath.heatBath_isMarkovKernel · instance · Teaching coverage

Statement

For every finite target and fixed selected coordinate under the construction's exact hypotheses, the coordinate heat-bath update is a Markov kernel on the full dependent product. At every starting state x its output law has total mass one, regardless of the target mass or whether the retained fiber has positive target mass.

\[\forall x\in S,\qquad K_i(x,S)=1.\]

All objects and hypotheses

{n : ℕ} — n is an arbitrary natural number, so Fin (n+1) is a nonempty finite index set. Individual coordinate spaces need not be finite.
(X : Fin (n + 1) → Type*) — X is a possibly dependent family: coordinate j may have its own type X j. A state x is a function choosing x j : X j for every j.
[∀ j, MeasurableSpace (X j)] — Each coordinate is measurable; the full and retained products use their product sigma-algebras.
(μ : Measure (∀ j, X j)) [IsFiniteMeasure μ] — μ is any finite measure on the full state space. It may have zero mass or be unnormalized.
(i : Fin (n + 1)) — i is a fixed selected coordinate, not a randomly drawn index.
[StandardBorelSpace (X i)] [Nonempty (X i)] — Only the selected coordinate must be nonempty and Standard Borel. The other coordinates need neither condition for the construction, Markovness, or invariance.

Notation and interpretation

S: The dependent full state space, written ∀ j, X j in Lean.
\[S=\prod_{j\in\operatorname{Fin}(n+1)}X_j\]
R_i: The retained-coordinate product. i.succAbove lists every original index except i; k is its own Fin n index.
\[R_i=\prod_{k\in\operatorname{Fin}(n)}X_{i.\operatorname{succAbove}(k)}\]
r_i: The tuple of all unselected coordinates; this is explanatory notation, not a newly introduced Lean declaration.
\[r_i(x)(k)=x(i.\operatorname{succAbove}(k))\]
e_i: MeasurableEquiv.piFinSuccAbove X i first places Xi before Ri; composing with prodComm puts retained coordinates first. e_i and its inverse are measurable.
\[e_i:S\simeq_{\mathrm{meas}}R_i\times X_i,\qquad e_i(x)=(r_i(x),x_i)\]
η_i,m_i,q_i: Pushed-forward joint target, retained marginal, and selected conditional version.
\[\eta_i=(e_i)_\#\mu,\qquad m_i=(\operatorname{fst})_\#\eta_i,\qquad q_i(r)=\operatorname{condDistrib}(\operatorname{snd}\mid\operatorname{fst};\eta_i)(r)\]
K_i: The existing public CoordinateHeatBath.heatBath X μ i; this evaluated formula uses HeatBath.heatBathSnd_apply.
\[K_i(x)=(e_i^{-1})_\#\bigl(\delta_{r_i(x)}\otimes q_i(r_i(x))\bigr)\]

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. Use the one-block probability law

The pushed-forward target ηi is finite and Xi has the required conditional-existence structures. Thus the existing one-block heat-bath kernel returns a probability law at every split input.

\[H_{\eta_i}(e_i(x),R_i\times X_i)=1.\]

Corresponding Lean step

After unfold heatBath, the implicit Markov instance for HeatBath.heatBathSnd is available.

2. Changing the input does not change the mass property

A comap simply substitutes e(x) for the input of the same kernel. It cannot change whether each output measure has mass one.

\[\operatorname{comap}_{e_i}H_{\eta_i}(x,R_i\times X_i)=H_{\eta_i}(e_i(x),R_i\times X_i)=1.\]

Corresponding Lean step

ProbabilityTheory.Kernel.IsMarkovKernel.comap is inferred for the comapped kernel.

3. A measurable pushforward of a probability measure is a probability measure

The inverse equivalence is measurable. The inverse image of the entire original state space is the entire split state space, so mapping the output through e⁻¹ preserves total mass one.

\[K_i(x,S)=H_{\eta_i}(e_i(x),(e_i^{-1})^{-1}(S))=H_{\eta_i}(e_i(x),R_i\times X_i)=1.\]

Corresponding Lean step

exact Kernel.IsMarkovKernel.map _ e.symm.measurable, written with the explicit equivalence expression in the original source.

Lean statement · heatBath_isMarkovKernel

Rewriting a state in different coordinates and then translating the result back does not lose probability mass. A whole probability distribution before the change of coordinates is still a whole probability distribution afterward.

instance heatBath_isMarkovKernel (μ : Measure (∀ j, X j)) [IsFiniteMeasure μ]
    (i : Fin (n + 1)) [StandardBorelSpace (X i)] [Nonempty (X i)] :
    IsMarkovKernel (heatBath X μ i)

Exact module and namespace context

Lean proof / instance · heatBath_isMarkovKernel

`Kernel.IsMarkovKernel.map` is the reused theorem, applied explicitly to the already-Markov comapped kernel. The underscore lets Lean infer which kernel is being mapped from the goal. `...symm.measurable` supplies measurability of the inverse coordinate change. There is no fallback to a nonmeasurable map. The instance proves only normalization. It does not identify which states the selected conditional measure favors on a null fiber.

instance heatBath_isMarkovKernel (μ : Measure (∀ j, X j)) [IsFiniteMeasure μ]
    (i : Fin (n + 1)) [StandardBorelSpace (X i)] [Nonempty (X i)] :
    IsMarkovKernel (heatBath X μ i) := by
  unfold heatBath
  exact Kernel.IsMarkovKernel.map _
    ((MeasurableEquiv.piFinSuccAbove X i).trans MeasurableEquiv.prodComm).symm.measurable

/-- Exact invariance by literal reuse of one-block heat-bath and measurable
kernel transport. No convergence from other initial laws is inferred. -/

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.IsMarkovKernel.map
ProbabilityTheory.Kernel.IsMarkovKernel.comap
MeasurableEquiv.piFinSuccAbove
MeasurableEquiv.prodComm

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.CoordinateHeatBath.heatBath_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) — Generic Markovness is checked with only the selected coordinate nonempty Standard Borel; no whole-product Standard Borel assumption is imposed.

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 coordinate update preserves the original finite target

AutoSamplingTheory.TechnicalLemmas.Probability.CoordinateHeatBath.heatBath_invariant · theorem · Teaching coverage

Statement

For every finite measure μ on the dependent coordinate product, a fixed selected coordinate's heat-bath kernel preserves μ, provided only that all coordinates are measurable and the selected coordinate is nonempty Standard Borel. No singleton-measurability, density, positive-support, or probability-normalization assumption is used.

\[K_i\circ_m\mu=\mu,\qquad \text{i.e. }\int_S K_i(x,A)\,\mu(dx)=\mu(A)\quad\text{for every measurable }A\subseteq S.\]

All objects and hypotheses

{n : ℕ} — n is an arbitrary natural number, so Fin (n+1) is a nonempty finite index set. Individual coordinate spaces need not be finite.
(X : Fin (n + 1) → Type*) — X is a possibly dependent family: coordinate j may have its own type X j. A state x is a function choosing x j : X j for every j.
[∀ j, MeasurableSpace (X j)] — Each coordinate is measurable; the full and retained products use their product sigma-algebras.
(μ : Measure (∀ j, X j)) [IsFiniteMeasure μ] — μ is any finite measure on the full state space. It may have zero mass or be unnormalized.
(i : Fin (n + 1)) — i is a fixed selected coordinate, not a randomly drawn index.
[StandardBorelSpace (X i)] [Nonempty (X i)] — Only the selected coordinate must be nonempty and Standard Borel. The other coordinates need neither condition for the construction, Markovness, or invariance.

Notation and interpretation

S: The dependent full state space, written ∀ j, X j in Lean.
\[S=\prod_{j\in\operatorname{Fin}(n+1)}X_j\]
R_i: The retained-coordinate product. i.succAbove lists every original index except i; k is its own Fin n index.
\[R_i=\prod_{k\in\operatorname{Fin}(n)}X_{i.\operatorname{succAbove}(k)}\]
r_i: The tuple of all unselected coordinates; this is explanatory notation, not a newly introduced Lean declaration.
\[r_i(x)(k)=x(i.\operatorname{succAbove}(k))\]
e_i: MeasurableEquiv.piFinSuccAbove X i first places Xi before Ri; composing with prodComm puts retained coordinates first. e_i and its inverse are measurable.
\[e_i:S\simeq_{\mathrm{meas}}R_i\times X_i,\qquad e_i(x)=(r_i(x),x_i)\]
η_i,m_i,q_i: Pushed-forward joint target, retained marginal, and selected conditional version.
\[\eta_i=(e_i)_\#\mu,\qquad m_i=(\operatorname{fst})_\#\eta_i,\qquad q_i(r)=\operatorname{condDistrib}(\operatorname{snd}\mid\operatorname{fst};\eta_i)(r)\]
K_i: The existing public CoordinateHeatBath.heatBath X μ i; this evaluated formula uses HeatBath.heatBathSnd_apply.
\[K_i(x)=(e_i^{-1})_\#\bigl(\delta_{r_i(x)}\otimes q_i(r_i(x))\bigr)\]

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. Move the invariant-law problem to split coordinates

Let e=e_i and η=e#μ. The one-block theorem already proves exact invariance of η under Hη.

\[H_\eta\circ_m\eta=\eta,\qquad\eta=e_\#\mu.\]

Corresponding Lean step

HeatBath.heatBathSnd_invariant (μ.map e).

2. Transport the proven invariant pair back

The existing KernelTransport theorem says that pushing both an invariant measure and the kernel's output through a measurable equivalence, while pulling the kernel input back, preserves invariance. Apply it to e⁻¹ and the invariant pair (Hη,η). This yields exactly the transported coordinate kernel.

\[\bigl((\operatorname{comap}_e H_\eta)\operatorname{.map}(e^{-1})\bigr)\circ_m (e^{-1})_\#\eta=(e^{-1})_\#\eta.\]

Corresponding Lean step

KernelTransport.invariant_map_comap e.symm (HeatBath.heatBathSnd_invariant (μ.map e)).

3. Cancel the inverse pushforward

Since e is a measurable equivalence, pushing μ through e and then back through e⁻¹ gives μ. Simplify the double inverse in the transported input and unfold heatBath to identify the target kernel.

\[(e^{-1})_\#(e_\#\mu)=\mu,\qquad(e^{-1})^{-1}=e,\qquad K_i\circ_m\mu=\mu.\]

Corresponding Lean step

simpa only [heatBath, MeasurableEquiv.symm_symm, MeasurableEquiv.map_symm_map] using the transport result.

Lean statement · heatBath_invariant

We already know the pair update preserves the target when the state is written as (retained coordinates, selected coordinate). Calling the same states by their original coordinate names cannot change that equality of laws.

theorem heatBath_invariant (μ : Measure (∀ j, X j)) [IsFiniteMeasure μ]
    (i : Fin (n + 1)) [StandardBorelSpace (X i)] [Nonempty (X i)] :
    (heatBath X μ i).Invariant μ

Exact module and namespace context

Lean proof · heatBath_invariant

`let e := ...` gives a local name to the existing measurable equivalence; it is not a new global definition. `invariant_map_comap e.symm` uses the inverse equivalence because we start from the split-space target and move back to original coordinates. `simpa only [...]` restricts simplification to exactly the listed definitional/equivalence facts, making the adapter visible. The transport theorem itself requires no Markovness or finiteness; those hypotheses enter through the particular heat-bath kernel being transported.

theorem heatBath_invariant (μ : Measure (∀ j, X j)) [IsFiniteMeasure μ]
    (i : Fin (n + 1)) [StandardBorelSpace (X i)] [Nonempty (X i)] :
    (heatBath X μ i).Invariant μ := by
  let e := (MeasurableEquiv.piFinSuccAbove X i).trans MeasurableEquiv.prodComm
  simpa only [heatBath, MeasurableEquiv.symm_symm, MeasurableEquiv.map_symm_map] using
    KernelTransport.invariant_map_comap e.symm (HeatBath.heatBathSnd_invariant (μ.map e))

/-- At each input `x`, every coordinate other than the selected one is retained
almost surely. Singleton measurability is needed only at the retained coordinate
`j`: equality of a marginal law with a Dirac measure on a coarse measurable
space would not alone imply literal almost-everywhere equality. -/

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)

MeasurableEquiv.piFinSuccAbove
MeasurableEquiv.prodComm
MeasurableEquiv.symm_symm
MeasurableEquiv.map_symm_map

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.CoordinateHeatBath.heatBath_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) — Covers generic invariance, zero targets, and an indiscrete retained coordinate. KernelMixture and KernelInvariance appear only in consumer tests, not as proof parents of this theorem.

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 unselected coordinate stays unchanged almost surely

AutoSamplingTheory.TechnicalLemmas.Probability.CoordinateHeatBath.heatBath_ae_apply_eq · theorem · Teaching coverage

Statement

Fix a finite target μ, selected coordinate i with Xi nonempty Standard Borel, and a distinct coordinate j whose singletons are measurable. At every input x, almost every output y under the actual transition law heatBath X μ i x satisfies y j = x j. The almost-everywhere quantifier is over the output law for each fixed input; it is not a statement only for μ-almost-every input, nor is it pointwise equality for every possible y.

\[\forall x\in S,\qquad y_j=x_j\quad\text{for }K_i(x)\text{-almost every }y.\qquad\text{Equivalently }K_i(x,\{y:y_j=x_j\})=1.\]

All objects and hypotheses

{n : ℕ} — n is an arbitrary natural number, so Fin (n+1) is a nonempty finite index set. Individual coordinate spaces need not be finite.
(X : Fin (n + 1) → Type*) — X is a possibly dependent family: coordinate j may have its own type X j. A state x is a function choosing x j : X j for every j.
[∀ j, MeasurableSpace (X j)] — Each coordinate is measurable; the full and retained products use their product sigma-algebras.
(μ : Measure (∀ j, X j)) [IsFiniteMeasure μ] — μ is any finite measure on the full state space. It may have zero mass or be unnormalized.
(i : Fin (n + 1)) — i is a fixed selected coordinate, not a randomly drawn index.
[StandardBorelSpace (X i)] [Nonempty (X i)] — Only the selected coordinate must be nonempty and Standard Borel. The other coordinates need neither condition for the construction, Markovness, or invariance.
(j : Fin (n + 1)) — j is one particular coordinate whose output is to be compared with the input.
[MeasurableSingletonClass (X j)] — Every singleton in X j is measurable. This makes the event y j = x j measurable. The other retained coordinates and their full product need no singleton assumption for this one-coordinate conclusion.
(hji : j ≠ i) — The coordinate j is not the selected coordinate.
(x : ∀ j, X j) — x is any input state, including an input with a marginal-null retained fiber.

Notation and interpretation

S: The dependent full state space, written ∀ j, X j in Lean.
\[S=\prod_{j\in\operatorname{Fin}(n+1)}X_j\]
R_i: The retained-coordinate product. i.succAbove lists every original index except i; k is its own Fin n index.
\[R_i=\prod_{k\in\operatorname{Fin}(n)}X_{i.\operatorname{succAbove}(k)}\]
r_i: The tuple of all unselected coordinates; this is explanatory notation, not a newly introduced Lean declaration.
\[r_i(x)(k)=x(i.\operatorname{succAbove}(k))\]
e_i: MeasurableEquiv.piFinSuccAbove X i first places Xi before Ri; composing with prodComm puts retained coordinates first. e_i and its inverse are measurable.
\[e_i:S\simeq_{\mathrm{meas}}R_i\times X_i,\qquad e_i(x)=(r_i(x),x_i)\]
η_i,m_i,q_i: Pushed-forward joint target, retained marginal, and selected conditional version.
\[\eta_i=(e_i)_\#\mu,\qquad m_i=(\operatorname{fst})_\#\eta_i,\qquad q_i(r)=\operatorname{condDistrib}(\operatorname{snd}\mid\operatorname{fst};\eta_i)(r)\]
K_i: The existing public CoordinateHeatBath.heatBath X μ i; this evaluated formula uses HeatBath.heatBathSnd_apply.
\[K_i(x)=(e_i^{-1})_\#\bigl(\delta_{r_i(x)}\otimes q_i(r_i(x))\bigr)\]
k,ν: k is the retained tuple's position corresponding to j; ν is a probability measure on Xi.
\[k\in\operatorname{Fin}(n),\quad i.\operatorname{succAbove}(k)=j,\qquad \nu=q_i(r_i(x))\]

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. Identify j inside the retained tuple

Because j≠i, the enumeration succAbove contains j. Choose k with i.succAbove(k)=j and rewrite the problem using this k. Set a=r_i(x) and ν=q_i(a).

\[\exists k\in\operatorname{Fin}(n),\quad i.\operatorname{succAbove}(k)=j,\qquad a=r_i(x),\quad \nu=q_i(a).\]

Corresponding Lean step

obtain ⟨k, rfl⟩ := Fin.exists_succAbove_eq hji; the local e and ν match the coordinate split.

2. Prove the retained evaluation is fixed under its Dirac law

The map z↦z(k) from Ri to Xj is measurable. Since {a(k)} is measurable in Xj, the event z(k)=a(k) is measurable and contains a, hence has full δa measure. Notice why measurability of singletons in the whole retained product is unnecessary.

\[\delta_a(\{z:z(k)=a(k)\})=1,\qquad z(k)=a(k)\quad\delta_a\text{-a.e.}\]

Corresponding Lean step

hret := ae_eq_dirac' (measurable_pi_apply k).

3. Compute the first marginal of the split output law

The conditional law ν is a probability measure, so the first marginal of δa⊗ν is ν(Xi) times δa, which is δa. This computation does not use target positivity or the conditional support of ν.

\[(\operatorname{fst})_\#(\delta_a\otimes\nu)=\nu(X_i)\,\delta_a=\delta_a.\]

Corresponding Lean step

hfirst is proved by simp [ν], using Measure.map_fst_prod and measure_univ for the conditional probability measure.

4. Pull the retained equality through the first projection

An event that holds almost everywhere for a pushforward measure also holds almost everywhere after composing with the measurable map. Apply this to fst and the Dirac-a.e. equality from step 2.

\[p_1(k)=a(k)\quad\text{for }(\delta_a\otimes\nu)\text{-almost every }p.\]

Corresponding Lean step

hprod := ae_of_ae_map measurable_fst.aemeasurable (by rw [hfirst]; exact hret).

5. Check that reconstruction reads the same coordinate

For every split output p, applying e and then evaluating its retained kth coordinate to the identity e(e⁻¹p)=p gives the exact coordinate formula for e⁻¹p. This is a pointwise algebraic identity, separate from the probabilistic a.e. statement.

\[e(e^{-1}p)=p\quad\Longrightarrow\quad(e^{-1}p)(i.\operatorname{succAbove}(k))=p_1(k).\]

Corresponding Lean step

hcoord p := congrArg (fun q => q.1 k) (e.apply_symm_apply p).

6. Push the almost-everywhere event back to original coordinates

Expand the public kernel to (e⁻¹)#(δa⊗ν). The event yj=xj is measurable because evaluation at j is measurable and {xj} is measurable. The measurable map a.e. equivalence reduces the goal to the split output. Combining hcoord with hprod gives the equality and hence the result.

\[(e^{-1}p)_j=p_1(k)=a(k)=x_j\quad(\delta_a\otimes\nu)\text{-a.e.},\quad\text{so }y_j=x_j\quad K_i(x)\text{-a.e.}\]

Corresponding Lean step

Kernel.map_apply, Kernel.comap_apply, HeatBath.heatBathSnd_apply; (ae_map_iff e.symm.measurable.aemeasurable ...).2; hprod.mono (fun p hp => (hcoord p).trans hp).

Lean statement · heatBath_ae_apply_eq

The selected coordinate may change, but the retained tuple enters the split output as a point mass. Reading coordinate j from that point mass fixes its old value with probability one. We must still check that the event 'this coordinate equals its old value' is measurable; that is what the singleton assumption does.

theorem heatBath_ae_apply_eq (μ : Measure (∀ j, X j)) [IsFiniteMeasure μ]
    (i : Fin (n + 1)) [StandardBorelSpace (X i)] [Nonempty (X i)]
    (j : Fin (n + 1)) [MeasurableSingletonClass (X j)] (hji : j ≠ i)
    (x : ∀ j, X j) :
    ∀ᵐ y ∂heatBath X μ i x, y j = x j

Exact module and namespace context

Lean proof · heatBath_ae_apply_eq

`∀ᵐ y ∂heatBath X μ i x, ...` means the property fails only on a set of zero measure for that one transition law. The input x is unrestricted. `obtain ⟨k, rfl⟩` chooses the retained index and replaces j by its equal expression, avoiding manual dependent-type casts. `hret`, `hfirst`, `hprod`, and `hcoord` are local proved facts: respectively the Dirac event, first marginal, lifted event, and inverse-coordinate identity. `congrArg` applies a function to both sides of an equality. Here it extracts the kth retained coordinate from the measurable equivalence's inverse law. `ae_map_iff ... .2` transports the almost-everywhere fact through the measurable inverse map; its explicit measurable-set proof is exactly where the singleton hypothesis is visible. `hprod.mono` replaces an almost-everywhere proposition by one it implies, using transitivity of the two coordinate equalities.

theorem heatBath_ae_apply_eq (μ : Measure (∀ j, X j)) [IsFiniteMeasure μ]
    (i : Fin (n + 1)) [StandardBorelSpace (X i)] [Nonempty (X i)]
    (j : Fin (n + 1)) [MeasurableSingletonClass (X j)] (hji : j ≠ i)
    (x : ∀ j, X j) :
    ∀ᵐ y ∂heatBath X μ i x, y j = x j := by
  obtain ⟨k, rfl⟩ := Fin.exists_succAbove_eq hji
  let e := (MeasurableEquiv.piFinSuccAbove X i).trans MeasurableEquiv.prodComm
  let ν := condDistrib Prod.snd Prod.fst (μ.map e) (e x).1
  have hret : ∀ᵐ z ∂Measure.dirac (e x).1, z k = (e x).1 k :=
    ae_eq_dirac' (measurable_pi_apply k)
  have hfirst : ((Measure.dirac (e x).1).prod ν).map Prod.fst =
      Measure.dirac (e x).1 := by
    simp [ν]
  have hprod : ∀ᵐ p ∂(Measure.dirac (e x).1).prod ν, p.1 k = (e x).1 k :=
    ae_of_ae_map measurable_fst.aemeasurable (by rw [hfirst]; exact hret)
  have hcoord (p : (∀ j, X (i.succAbove j)) × X i) :
      e.symm p (i.succAbove k) = p.1 k :=
    congrArg (fun q => q.1 k) (e.apply_symm_apply p)
  change ∀ᵐ y ∂((HeatBath.heatBathSnd (μ.map e)).comap e e.measurable).map e.symm x,
    y (i.succAbove k) = x (i.succAbove k)
  rw [Kernel.map_apply _ e.symm.measurable, Kernel.comap_apply, HeatBath.heatBathSnd_apply]
  apply (ae_map_iff e.symm.measurable.aemeasurable
    ((measurable_pi_apply (i.succAbove k)) (measurableSet_singleton _))).2
  change ∀ᵐ p ∂(Measure.dirac (e x).1).prod ν,
    e.symm p (i.succAbove k) = (e x).1 k
  exact hprod.mono (fun p hp => (hcoord p).trans hp)

end AutoSamplingTheory.TechnicalLemmas.Probability.CoordinateHeatBath

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.
Retaining coordinates almost surely at every input is not a Gibbs/feasible-support assertion for the selected conditional version on a null retained fiber.
The theorem is one retained-coordinate assertion at a time. A tests-only finite-intersection consumer proves simultaneous retention assuming singleton measurability at every coordinate; it is not another public declaration in this module.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

Fin.exists_succAbove_eq
MeasurableEquiv.piFinSuccAbove
MeasurableEquiv.prodComm
MeasureTheory.ae_eq_dirac'
measurable_pi_apply
MeasureTheory.Measure.map_fst_prod
MeasureTheory.measure_univ
MeasureTheory.ae_of_ae_map
MeasurableEquiv.apply_symm_apply
ProbabilityTheory.Kernel.map_apply
ProbabilityTheory.Kernel.comap_apply
MeasureTheory.ae_map_iff
measurableSet_singleton

The local hfirst uses simp's existing conditional-kernel Markov instance. KernelMixture/KernelInvariance are tests-only consumers.

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.CoordinateHeatBath.heatBath_ae_apply_eq — 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 simultaneous retention by a finite intersection, a middle update on Fin 3 → Bool, and a nonconstant input with zero target. An indiscrete retained coordinate deliberately receives only marginal-law/invariance tests: no literal a.e. equality is asserted without its singleton contract.

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