Ordinary-Wasserstein control gives an SPHMC phase-state moment
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseStateMoment.phase_state_second_moment_of_wasserstein · theorem · Teaching coverage
Mathematical statement
The incoming phase energy is integrable and at most 2(Mx+Mp)+4r².
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.
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 ^ 2Proof 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.
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.
Corresponding Lean step
LipschitzWith.prod_snd.
3. Transfer both moments
Apply the shared theorem independently to position and momentum, preserving both integrability conclusions.
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.
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.
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.
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.PhaseStateMomentScope 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
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.