Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
Samplinglib mathematical lesson

Every unselected coordinate stays unchanged almost surely

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

Read this first

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

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

Download module (.lean)
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

Proof roadmap

  1. 1Identify 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).

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

  3. 3Compute 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 ν.

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

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

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

Full assumptions and notation

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 verification

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

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.

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

Download module (.lean)
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.
Sources, dependencies, and reuse

Source and reuse

Samplinglib 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

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

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