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

SPHMC initial phase coupling, q=2 proof edge

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang. ASTIS supplies the measure-theoretic coupling construction.

arXiv:2609.06906v1 · Lemma 4.16 proof, identical-momentum coupling · faithful paraphrase

Complete source statement (Samplinglib restatement)

Lemma 4.16 bounds W_{q,M_kappa} between delta_xref tensor N(0,I) and Pi_eta for all q at least 2. Its proof couples momenta identically. This bounded ASTIS proof edge constructs that coupling and proves its exact q=2 Kantorovich cost estimate for any position probability measure with a finite second moment.

  • Finite-dimensional real inner-product Borel space.
  • Position probability law with integrable squared distance to xref.
  • kappa at least one and the paper's exact phase metric.

Actual phase laws

\[\mu_0=\delta_{x_{\rm ref}}\otimes\gamma,\qquad\Pi=\pi\otimes\gamma.\]

Identical momentum cost

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

Squared transport bound

\[W_{2,M_\kappa}^{2}(\mu_0,\Pi)\le\int\|x_{\rm ref}-y\|^2\,\pi(dy).\]

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

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

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

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

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

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 ∂π) := 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

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
The paper's Lemma 4.16 uses the smoothed Gibbs target Pi_eta.The coupling-cost theorem accepts any position probability law with an integrable second moment about xref.generalizationThe identical-momentum coupling uses no Gibbs structure; the specialized numeric estimate is a separate remaining proof edge.
Lemma 4.16 concludes a W_q estimate for every q at least two.The statement bounds the squared M_kappa Kantorovich cost, corresponding only to q=2.source-implicitThis declaration binds only the explicit same-momentum proof component and does not claim the all-q source obligation.

Only the generic q=2 coupling cost; no Gibbs numeric bound, all-q concentration, Picard history or query cost.

Encoder–denoiser: source-reviewed · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

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

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

Which proof obligations and prerequisites are covered?

  • Formalized proof edge; source adapter/review separate Construct the exact same-momentum coupling and bound its q=2 cost
  • TODO — not closed by these contributions Insert smoothed Gibbs moment and small-gradient reference-point bound (remaining)
  • TODO — not closed by these contributions Strong-log-concavity concentration for every q at least two (remaining)
  • TODO — not closed by these contributions Algorithm-history estimate D.3 (remaining, separate)