Samplinglib mathematical lesson

Couple the initial and reference phase laws with identical momentum

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.InitialPhaseTransport.phaseWassersteinSq_initial_le_position_moment · theorem · Teaching coverage

Read this first

Mathematical statement

The actual initial phase law at xref and any product reference law with standard-Gaussian momentum admit a coupling that uses the same momentum on both sides. Its M-kappa transportation cost is at most the reference law's position second moment about xref.

\[W_{2,M_\kappa}^{2}(\delta_{x_{\rm ref}}\otimes\gamma,\,\pi\otimes\gamma)\le\int\|x_{\rm ref}-y\|^2\,\pi(dy),\qquad\kappa\ge1,\quad\gamma=\mathsf N(0,I).\]

Lean statement · phaseWassersteinSq_initial_le_position_moment

The result controls the squared Kantorovich value directly. It is generic in the position law, so the paper's smoothed Gibbs law must still be supplied by a separate specialization.

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 phaseWassersteinSq_initial_le_position_moment
    (π : Measure E) [IsProbabilityMeasure π] (xref : E)
    {κ : ℝ} (hκ : 1 ≤ κ)
    (hpos : Integrable (fun y : E => ‖xref - y‖ ^ 2) π) :
    PhaseMetric.phaseWassersteinSq κ
      ((Measure.dirac xref).prod (stdGaussian E))
      (π.prod (stdGaussian E)) ≤
        ENNReal.ofReal (∫ y : E, ‖xref - y‖ ^ 2 ∂π)

Exact module and namespace context

Proof roadmap

1Build the actual coupling
Draw Y from pi and P independently from the standard Gaussian; pair the phase states (xref,P) and (Y,P). The first and second marginals are exactly the required phase laws.
2Cancel the momentum displacement
For a paired sample the momentum difference is zero. The paper's twisted quadratic form therefore reduces to its position coefficient, which is at most one when kappa is at least one.
3Bound the Kantorovich infimum
Any admissible coupling upper-bounds the optimal transport cost. Measurability permits pushforward integration, and the finite position moment converts the nonnegative Lebesgue integral back to the ordinary expectation.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional complete real inner-product Borel space.
The target position law pi is a probability measure with an integrable squared distance from xref.
The paper phase parameter kappa is at least one; its M_kappa quadratic form is used without changing normalization.
Both phase laws use the same standard-Gaussian momentum marginal.

Mathematical proof

1. Build the actual coupling

Draw Y from pi and P independently from the standard Gaussian; pair the phase states (xref,P) and (Y,P). The first and second marginals are exactly the required phase laws.

\[\Gamma=\operatorname{Law}((x_{\rm ref},P),(Y,P)),\quad\Gamma_1=\delta_{x_{\rm ref}}\otimes\gamma,\quad\Gamma_2=\pi\otimes\gamma.\]

Corresponding Lean step

identicalMomentumCoupling; Measure.fst_map_prodMk, Measure.snd_map_prodMk and Measure.dirac_prod certify both marginals.

2. Cancel the momentum displacement

For a paired sample the momentum difference is zero. The paper's twisted quadratic form therefore reduces to its position coefficient, which is at most one when kappa is at least one.

\[\|(x_{\rm ref},P)-(Y,P)\|_{M_\kappa}^2=\left(\frac1{2\kappa}+\frac12\right)\|x_{\rm ref}-Y\|^2\le\|x_{\rm ref}-Y\|^2.\]

Corresponding Lean step

phaseCost_identical_momentum_le unfolds the exact phase cost and proves the coefficient inequality.

3. Bound the Kantorovich infimum

Any admissible coupling upper-bounds the optimal transport cost. Measurability permits pushforward integration, and the finite position moment converts the nonnegative Lebesgue integral back to the ordinary expectation.

\[\inf_{\Lambda\in\mathsf{Cpl}(\mu_0,\Pi)}\int c_{M_\kappa}\,d\Lambda\le\int c_{M_\kappa}\,d\Gamma\le\mathbb E_\pi\|x_{\rm ref}-Y\|^2.\]

Corresponding Lean step

Transport.transportCost_le_lintegral_of_isCoupling, lintegral_map, lintegral_mono and ofReal_integral_eq_lintegral_ofReal.

Lean verification

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

Lean proof · phaseWassersteinSq_initial_le_position_moment

The proof constructs an explicit pushforward coupling; it does not assume existence of an optimal coupling. Product-law measurability and square integrability justify the cost calculation.

Download module (.lean)

theorem phaseWassersteinSq_initial_le_position_moment
    (π : Measure E) [IsProbabilityMeasure π] (xref : E)
    {κ : ℝ} (hκ : 1 ≤ κ)
    (hpos : Integrable (fun y : E => ‖xref - y‖ ^ 2) π) :
    PhaseMetric.phaseWassersteinSq κ
      ((Measure.dirac xref).prod (stdGaussian E))
      (π.prod (stdGaussian E)) ≤
        ENNReal.ofReal (∫ y : E, ‖xref - y‖ ^ 2 ∂π) := by
  let γ := identicalMomentumCoupling π xref
  have hγ := identicalMomentumCoupling_isCoupling π xref
  have hcost := Transport.transportCost_le_lintegral_of_isCoupling
    (PhaseMetric.phaseCost (E := E) κ) _ _ γ hγ
  change PhaseMetric.phaseWassersteinSq κ _ _ ≤ _
  refine hcost.trans ?_
  have hmeas : Measurable (PhaseMetric.phaseCost (E := E) κ) := by
    unfold PhaseMetric.phaseCost
    change Measurable (fun z : (E × E) × (E × E) =>
      ENNReal.ofReal ((1 / (2 * κ) + 1 / 2) * ‖(z.1 - z.2).1‖ ^ 2 +
        inner ℝ (z.1 - z.2).1 (z.1 - z.2).2 + ‖(z.1 - z.2).2‖ ^ 2))
    fun_prop
  rw [show γ = (π.prod (stdGaussian E)).map (fun z => ((xref, z.2), z)) by rfl,
    lintegral_map hmeas (by fun_prop)]
  have hbound : (∫⁻ z : E × E,
      PhaseMetric.phaseCost κ ((xref, z.2), z) ∂π.prod (stdGaussian E)) ≤
      ∫⁻ z : E × E, ENNReal.ofReal (‖xref - z.1‖ ^ 2) ∂π.prod (stdGaussian E) := by
    apply lintegral_mono
    intro z
    exact phaseCost_identical_momentum_le hκ xref z.1 z.2
  refine hbound.trans_eq ?_
  rw [← ofReal_integral_eq_lintegral_ofReal
    (hpos.comp_fst (stdGaussian E))
    (Filter.Eventually.of_forall fun z => sq_nonneg _)]
  congr 1
  rw [integral_prod _ (hpos.comp_fst (stdGaussian E))]
  simp

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.InitialPhaseTransport

Exact module and namespace context

Scope and omitted-condition boundaries

This is only the q=2 coupling-cost edge in the proof of SPHMC Lemma 4.16. It does not yet insert Gibbs concentration or the small-gradient reference-point bound, establish q>2, or control any Picard trajectory.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Measure.fst_map_prodMk
Measure.snd_map_prodMk
Measure.dirac_prod
lintegral_map
ofReal_integral_eq_lintegral_ofReal

Mathematical sources

Smoothed Picard Hamiltonian Monte Carlo, Lemma 4.16 proof — ASTIS expands the source's identical-momentum coupling and the precise Kantorovich-cost estimate.

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