On a positive retained fiber, the update is normalized target restriction

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

Statement

Let μ be any finite measure on a finite dependent product of measurable coordinate spaces. Fix i with Xi nonempty Standard Borel, assume measurable singletons in the retained product Ri, and choose x whose retained fiber Fi(x) has nonzero μ mass. Then the actual coordinate heat-bath output measure at x equals μ restricted to Fi(x), scaled by the reciprocal of its mass. Thus for every measurable event A in the full state space, the transition probability is μ(Fi(x)∩A)/μ(Fi(x)). This is an equality of whole output measures at this fixed positive fiber, not merely a selected-coordinate marginal identity.

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.
• [MeasurableSingletonClass (∀ j : Fin n, X (i.succAbove j))] — The retained product Ri has measurable singletons. This makes its conditioning atom {r_i(x)} and the full-state fiber Fi(x) measurable. It is a separate assumption from the selected coordinate's Standard Borel structure; no Standard Borel assumption is added on Ri.
• (x : ∀ j, X j) — x is a fixed input state.
• (hx : μ {y | (fun j => y (i.succAbove j)) = (fun j => x (i.succAbove j))} ≠ 0) — The entire retained fiber has nonzero μ mass. Because μ is finite, this is exactly 0 < μ(Fi(x)) < ∞. It is not the stronger assumption μ{x}>0, although that would suffice by inclusion.

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)\]

F_i(x)

The retained fiber through x; its defining equality is equality of retained dependent tuples, not equality of just one coordinate.

\[F_i(x)=\{y\in S:r_i(y)=r_i(x)\}=r_i^{-1}(\{r_i(x)\})\]

cond(μ,F)

Mathlib's totalized normalized restriction. Its measurable-set values are μ(F)⁻¹ μ(F∩A), with arithmetic in the extended nonnegative reals.

\[\operatorname{cond}(\mu,F)=\mu(F)^{-1}\,\mu|_F\]

a,g,B

Local proof notation for the retained atom, the insertion map from Xi to S, and the preimage of a measurable test set A.

\[a=r_i(x),\qquad g(b)=e_i^{-1}(a,b),\qquad B=g^{-1}(A)\]

• 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

theorem heatBath_eq_cond (X : Fin (n + 1) → Type*) [∀ j, MeasurableSpace (X j)]
    (μ : Measure (∀ j, X j)) [IsFiniteMeasure μ]
    (i : Fin (n + 1)) [StandardBorelSpace (X i)] [Nonempty (X i)]
    [MeasurableSingletonClass (∀ j : Fin n, X (i.succAbove j))]
    (x : ∀ j, X j)
    (hx : μ {y | (fun j => y (i.succAbove j)) = (fun j => x (i.succAbove j))} ≠ 0) :
    heatBath X μ i x =
      cond μ {y | (fun j => y (i.succAbove j)) = (fun j => x (i.succAbove j))}

theorem heatBath_eq_cond (X : Fin (n + 1) → Type*) [∀ j, MeasurableSpace (X j)]
    (μ : Measure (∀ j, X j)) [IsFiniteMeasure μ]
    (i : Fin (n + 1)) [StandardBorelSpace (X i)] [Nonempty (X i)]
    [MeasurableSingletonClass (∀ j : Fin n, X (i.succAbove j))]
    (x : ∀ j, X j)
    (hx : μ {y | (fun j => y (i.succAbove j)) = (fun j => x (i.succAbove j))} ≠ 0) :
    heatBath X μ i x =
      cond μ {y | (fun j => y (i.succAbove j)) = (fun j => x (i.succAbove j))} := by
  let e := (MeasurableEquiv.piFinSuccAbove X i).trans MeasurableEquiv.prodComm
  have hm : (μ.map e).map Prod.fst {(e x).1} ≠ 0 := by
    rwa [Measure.map_apply measurable_fst (measurableSet_singleton _),
      Measure.map_apply e.measurable (measurable_fst (measurableSet_singleton _))]
  apply Measure.ext
  intro s hs
  change (((HeatBath.heatBathSnd (μ.map e)).comap e e.measurable).map e.symm x) s = _
  rw [Kernel.map_apply _ e.symm.measurable, Kernel.comap_apply,
    HeatBath.heatBathSnd_apply, Measure.dirac_prod,
    Measure.map_map e.symm.measurable measurable_prodMk_left,
    Measure.map_apply (e.symm.measurable.comp measurable_prodMk_left) hs,
    condDistrib_apply_of_ne_zero measurable_snd _ hm]
  simp only [Prod.eta, Measure.map_id']
  rw [Measure.map_apply e.measurable
    ((measurableSet_singleton _).prod ((e.symm.measurable.comp measurable_prodMk_left) hs)),
    Measure.map_apply measurable_fst (measurableSet_singleton _),
    Measure.map_apply e.measurable (measurable_fst (measurableSet_singleton _)),
    cond_apply' hs]
  congr 1
  congr 1
  ext y
  change ((e y).1 = (e x).1 ∧ e.symm ((e x).1, (e y).2) ∈ s) ↔
    ((e y).1 = (e x).1 ∧ y ∈ s)
  constructor
  · rintro ⟨hy, hys⟩
    refine ⟨hy, ?_⟩
    simpa only [← hy, Prod.eta, e.symm_apply_apply] using hys
  · rintro ⟨hy, hys⟩
    refine ⟨hy, ?_⟩
    simpa only [← hy, Prod.eta, e.symm_apply_apply] using hys

end AutoSamplingTheory.TechnicalLemmas.Probability.CoordinateHeatBath

Worked example

S=Fin 3→Bool; a=(false,false,false), b=(false,true,false), c=(true,false,false), off=(false,false,true). Target μ=(1/6)δa+(1/2)δb+(1/3)δc and selected coordinate i=1.

a and b have the same retained coordinates 0 and 2, so their masses normalize by 2/3; c differs at retained coordinate 0 and is excluded.

Why the positive-fiber hypothesis matters

The target is a nonzero probability measure, yet off has a null retained fiber. The normalized restriction has mass zero and cannot equal the always-Markov selected update. This is a counterexample to dropping hx, not a counterexample to the source algorithm's supported-start convention.

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.
• Finite coordinate count is not finite state space. The theorem does not require positive mass for every configuration or impose Standard Borel structure on all retained coordinates.
• Under μ(Fi(x))≠0 and finiteness, the normalized restriction is a probability law and has full mass on the measurable retained fiber. Neither this formula nor conditional-support conclusions extend to μ-null fibers.
• Positive singleton starting mass μ{x}≠0 suffices by {x}⊆Fi(x), but that implication is a private test adapter, not a second public theorem in this module.
• Do not present the formula as a random-site scan theorem, a concrete Gibbs target normalization, or accepted fidelity to the literal conflicting source copy step.