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.

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

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

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

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.