Samplinglib mathematical lesson

Ordinary-Wasserstein control gives an SPHMC phase-state moment

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseStateMoment.phase_state_second_moment_of_wasserstein · theorem · Teaching coverage

Read this first

Mathematical statement

The incoming phase energy is integrable and at most 2(Mx+Mp)+4r².

\[\mathbb E_\nu[\|X-x_\star\|^2+\|P\|^2]\le2(M_X+M_P)+4r^2.\]

Lean statement · phase_state_second_moment_of_wasserstein

The metric and every reference moment premise are visible; no stationary-law or history premise is hidden.

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 phase_state_second_moment_of_wasserstein
    (nu reference : Measure (E × E)) (xstar : E) {r Mx Mp : ℝ}
    (hX : Integrable (fun z : E × E => ‖z.1 - xstar‖ ^ 2) reference)
    (hP : Integrable (fun z : E × E => ‖z.2‖ ^ 2) reference)
    (hXbound : (∫ z : E × E, ‖z.1 - xstar‖ ^ 2 ∂reference) ≤ Mx)
    (hPbound : (∫ z : E × E, ‖z.2‖ ^ 2 ∂reference) ≤ Mp)
    (hW : WassersteinSpace.wassersteinDistance nu reference ^ 2 ≤
      ENNReal.ofReal (r ^ 2)) :
    Integrable (fun z : E × E => ‖z.1 - xstar‖ ^ 2 + ‖z.2‖ ^ 2) nu ∧
      (∫ z : E × E, ‖z.1 - xstar‖ ^ 2 + ‖z.2‖ ^ 2 ∂nu) ≤
        2 * (Mx + Mp) + 4 * r ^ 2

Exact module and namespace context

Proof roadmap

1Position is a one-Lipschitz observable
For the max product metric, projecting to position and subtracting xstar cannot increase distance.
2Momentum is a one-Lipschitz observable
The second product projection is one-Lipschitz for the same metric.
3Transfer both moments
Apply the shared theorem independently to position and momentum, preserving both integrability conclusions.
4Add only after integrability
Bochner integral additivity is now legal; adding the bounds gives the combined phase energy.

Full assumptions and notation

All objects and hypotheses

The reference phase law has integrable position and momentum squares, bounded respectively by Mx and Mp.
The incoming law is within ordinary squared W2 radius r² of the reference law.
The state space is finite-dimensional real inner-product Borel; completeness is not needed by this theorem.

Mathematical proof

1. Position is a one-Lipschitz observable

For the max product metric, projecting to position and subtracting xstar cannot increase distance.

\[g_X(x,p)=x-x_\star,\quad\operatorname{Lip}(g_X)\le1.\]

Corresponding Lean step

LipschitzWith.of_dist_le_mul and Prod.dist_eq.

2. Momentum is a one-Lipschitz observable

The second product projection is one-Lipschitz for the same metric.

\[g_P(x,p)=p,\quad\operatorname{Lip}(g_P)\le1.\]

Corresponding Lean step

LipschitzWith.prod_snd.

3. Transfer both moments

Apply the shared theorem independently to position and momentum, preserving both integrability conclusions.

\[I_X\le2M_X+2r^2,\qquad I_P\le2M_P+2r^2.\]

Corresponding Lean step

Two calls to of_wassersteinDistance_sq_le.

4. Add only after integrability

Bochner integral additivity is now legal; adding the bounds gives the combined phase energy.

\[I_X+I_P\le2(M_X+M_P)+4r^2.\]

Corresponding Lean step

Integrable.add, integral_add, and linear arithmetic.

Lean verification

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

Lean proof · phase_state_second_moment_of_wasserstein

Instantiate the shared observable theorem with the two phase projections and add the resulting integrable moments.

Download module (.lean)

theorem phase_state_second_moment_of_wasserstein
    (nu reference : Measure (E × E)) (xstar : E) {r Mx Mp : ℝ}
    (hX : Integrable (fun z : E × E => ‖z.1 - xstar‖ ^ 2) reference)
    (hP : Integrable (fun z : E × E => ‖z.2‖ ^ 2) reference)
    (hXbound : (∫ z : E × E, ‖z.1 - xstar‖ ^ 2 ∂reference) ≤ Mx)
    (hPbound : (∫ z : E × E, ‖z.2‖ ^ 2 ∂reference) ≤ Mp)
    (hW : WassersteinSpace.wassersteinDistance nu reference ^ 2 ≤
      ENNReal.ofReal (r ^ 2)) :
    Integrable (fun z : E × E => ‖z.1 - xstar‖ ^ 2 + ‖z.2‖ ^ 2) nu ∧
      (∫ z : E × E, ‖z.1 - xstar‖ ^ 2 + ‖z.2‖ ^ 2 ∂nu) ≤
        2 * (Mx + Mp) + 4 * r ^ 2 := by
  have hXlip : LipschitzWith 1 (fun z : E × E => z.1 - xstar) := by
    refine LipschitzWith.of_dist_le_mul ?_
    intro a b
    rw [NNReal.coe_one, one_mul, Prod.dist_eq]
    simpa only [dist_eq_norm, sub_sub_sub_cancel_right] using
      (le_max_left (dist a.1 b.1) (dist a.2 b.2))
  have hPlip : LipschitzWith 1 (fun z : E × E => z.2) :=
    LipschitzWith.prod_snd
  have hXt := WassersteinLipschitzMoment.of_wassersteinDistance_sq_le hXlip hX hW
  have hPt := WassersteinLipschitzMoment.of_wassersteinDistance_sq_le hPlip hP hW
  refine ⟨hXt.1.add hPt.1, ?_⟩
  rw [integral_add hXt.1 hPt.1]
  norm_num at hXt hPt
  linarith

end

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseStateMoment

Exact module and namespace context

Scope and omitted-condition boundaries

The premise uses Lean's ordinary product max metric, not the paper's M_kappa metric. The theorem does not prove (D.3), a run-history invariant, layer-center moments, (D.7) or (D.8).

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinLipschitzMoment.of_wassersteinDistance_sq_le

Mathlib API called (external library)

LipschitzWith.prod_snd
Prod.dist_eq
MeasureTheory.integral_add

Mathematical sources

Chen–Chewi–Lu–Zhang, Lemma D.4 proof — The phase-state second-moment transition after (D.3), with the metric comparison intentionally left separate.

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