Samplinglib mathematical lesson

Twisted SPHMC transport gives the phase-state second moment

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseMetric.phase_state_second_moment_of_phaseWasserstein · theorem · Teaching coverage

Read this first

Mathematical statement

The incoming phase energy is integrable and bounded by 2(Mx+Mp)+24r^2.

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

Lean statement · phase_state_second_moment_of_phaseWasserstein

All reference integrability and moment assumptions remain visible.

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_phaseWasserstein
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (nu reference : Measure (E × E)) (xstar : E) {kappa r Mx Mp : ℝ}
    (hkappa : 1 ≤ kappa)
    (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 : phaseWassersteinSq kappa nu reference ≤ 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) + 24 * r ^ 2

Exact module and namespace context

Proof roadmap

1Convert the radius
The uniform metric comparison gives the ordinary radius sqrt(6)|r|.
2Reuse the compiled coordinate theorem
The earlier theorem proves both integrability and the ordinary-Wasserstein moment estimate.
3Normalize the constant
Expand the square to obtain the explicit final factor.

Full assumptions and notation

All objects and hypotheses

kappa≥1.
Reference position and momentum squares are integrable and bounded by Mx,Mp.
The incoming law has M-kappa squared transport radius at most r^2.

Mathematical proof

1. Convert the radius

The uniform metric comparison gives the ordinary radius sqrt(6)|r|.

\[W_2^2\le6r^2=(\sqrt6\,r)^2.\]

Corresponding Lean step

wassersteinDistance_sq_le_phaseWassersteinSq and Real.sq_sqrt.

2. Reuse the compiled coordinate theorem

The earlier theorem proves both integrability and the ordinary-Wasserstein moment estimate.

\[I\le2(M_X+M_P)+4(\sqrt6r)^2.\]

Corresponding Lean step

PhaseStateMoment.phase_state_second_moment_of_wasserstein.

3. Normalize the constant

Expand the square to obtain the explicit final factor.

\[4(\sqrt6r)^2=24r^2.\]

Corresponding Lean step

Real.sq_sqrt and ring.

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_phaseWasserstein

Metric comparison followed by the already audited general moment adapter.

Download module (.lean)

theorem phase_state_second_moment_of_phaseWasserstein
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (nu reference : Measure (E × E)) (xstar : E) {kappa r Mx Mp : ℝ}
    (hkappa : 1 ≤ kappa)
    (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 : phaseWassersteinSq kappa nu reference ≤ 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) + 24 * r ^ 2 := by
  have hsqrt : Real.sqrt 6 ^ 2 = 6 := Real.sq_sqrt (by norm_num)
  have hordinary : WassersteinSpace.wassersteinDistance nu reference ^ 2 ≤
      ENNReal.ofReal ((Real.sqrt 6 * r) ^ 2) := by
    refine (wassersteinDistance_sq_le_phaseWassersteinSq hkappa nu reference).trans ?_
    calc
      ENNReal.ofReal 6 * phaseWassersteinSq kappa nu reference ≤
          ENNReal.ofReal 6 * ENNReal.ofReal (r ^ 2) := by gcongr
      _ = ENNReal.ofReal ((Real.sqrt 6 * r) ^ 2) := by
        rw [← ENNReal.ofReal_mul (by norm_num : (0 : ℝ) ≤ 6)]
        congr 1
        rw [mul_pow, hsqrt]
  have h := PhaseStateMoment.phase_state_second_moment_of_wasserstein
    nu reference xstar hX hP hXbound hPbound hordinary
  refine ⟨h.1, h.2.trans_eq ?_⟩
  rw [mul_pow, hsqrt]
  ring

end

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseMetric

Exact module and namespace context

Scope and omitted-condition boundaries

Consumes a twisted transport bound; does not prove the paper's (D.3), history estimate, D.7 or D.8.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseStateMoment.phase_state_second_moment_of_wasserstein

Mathlib API called (external library)

Real.sq_sqrt

Mathematical sources

Lemma D.4 proof after (D.3) — Metric conversion and coordinate-moment step.

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