Samplinglib mathematical lesson

Wasserstein distance transfers a Lipschitz observable's second moment

AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinLipschitzMoment.of_wassersteinDistance_sq_le · theorem · Teaching coverage

Read this first

Mathematical statement

The observable remains square-integrable under μ, and its μ second moment is bounded by twice its reference second moment plus 2b²r².

\[W_2^2(\mu,\nu)\le r^2\Longrightarrow \int\|g\|^2d\mu\le 2\int\|g\|^2d\nu+2b^2r^2.\]

Lean statement · of_wassersteinDistance_sq_le

The statement explicitly returns Integrable before its real-valued integral inequality.

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 of_wassersteinDistance_sq_le {mu nu : Measure E}
    {g : E → F} {b : ℝ≥0} {r : ℝ} (hg : LipschitzWith b g)
    (hi : Integrable (fun x => ‖g x‖ ^ 2) nu)
    (hw : WassersteinSpace.wassersteinDistance mu nu ^ 2 ≤ ENNReal.ofReal (r ^ 2)) :
    Integrable (fun x => ‖g x‖ ^ 2) mu ∧
      (∫ x, ‖g x‖ ^ 2 ∂mu) ≤
        2 * (∫ x, ‖g x‖ ^ 2 ∂nu) + 2 * (b : ℝ) ^ 2 * r ^ 2

Exact module and namespace context

Proof roadmap

1Choose an almost-optimal coupling
For every s>r², the definition of transport cost supplies a coupling whose quadratic cost is below s. Optimal-plan existence is unnecessary.
2Dominate the transported observable
Lipschitz continuity and the quadratic two-term inequality control the first-coordinate observable by an integrable reference term plus coupling displacement.
3Use the exact marginals
The coordinate projections of γ preserve μ and ν, so the two coupling integrals are exactly the desired marginal moments.
4Remove the excess cost
The bound holds for every s>r². Applying it at a controlled positive excess and letting that excess be arbitrary gives the closed r² bound.

Full assumptions and notation

All objects and hypotheses

E is a second-countable Borel normed additive group and F is a normed additive group.
g:E→F is b-Lipschitz and its squared norm is integrable under the reference law ν.
The squared extended-real Wasserstein distance from μ to ν is at most ofReal(r²).

Mathematical proof

1. Choose an almost-optimal coupling

For every s>r², the definition of transport cost supplies a coupling whose quadratic cost is below s. Optimal-plan existence is unnecessary.

\[\exists\gamma\in\Gamma(\mu,\nu):\int\|x-y\|^2d\gamma\le s.\]

Corresponding Lean step

wassersteinDistance_sq and exists_isCoupling_lintegral_lt_of_transportCost_lt.

2. Dominate the transported observable

Lipschitz continuity and the quadratic two-term inequality control the first-coordinate observable by an integrable reference term plus coupling displacement.

\[\|g(x)\|^2\le2\|g(y)\|^2+2b^2\|x-y\|^2.\]

Corresponding Lean step

The private pointwise bound and Integrable.mono' establish integrability before integral comparison.

3. Use the exact marginals

The coordinate projections of γ preserve μ and ν, so the two coupling integrals are exactly the desired marginal moments.

\[(\mathrm{fst})_\#\gamma=\mu,\quad(\mathrm{snd})_\#\gamma=\nu.\]

Corresponding Lean step

CouplingQuadraticIntegrability.measurePreserving_fst/snd_of_isCoupling.

4. Remove the excess cost

The bound holds for every s>r². Applying it at a controlled positive excess and letting that excess be arbitrary gives the closed r² bound.

\[\forall\varepsilon>0,\ I_\mu\le2I_\nu+2b^2r^2+\varepsilon.\]

Corresponding Lean step

le_of_forall_pos_le_add and real algebra close the infimum argument.

Lean verification

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

Lean proof · of_wassersteinDistance_sq_le

Approximate coupling, pointwise quadratic domination, marginal pushforward identities, then an epsilon closure argument.

Download module (.lean)

theorem of_wassersteinDistance_sq_le {mu nu : Measure E}
    {g : E → F} {b : ℝ≥0} {r : ℝ} (hg : LipschitzWith b g)
    (hi : Integrable (fun x => ‖g x‖ ^ 2) nu)
    (hw : WassersteinSpace.wassersteinDistance mu nu ^ 2 ≤ ENNReal.ofReal (r ^ 2)) :
    Integrable (fun x => ‖g x‖ ^ 2) mu ∧
      (∫ x, ‖g x‖ ^ 2 ∂mu) ≤
        2 * (∫ x, ‖g x‖ ^ 2 ∂nu) + 2 * (b : ℝ) ^ 2 * r ^ 2 := by
  have hall (s : ℝ) (hs : r ^ 2 < s) :
      Integrable (fun x => ‖g x‖ ^ 2) mu ∧
        (∫ x, ‖g x‖ ^ 2 ∂mu) ≤
          2 * (∫ x, ‖g x‖ ^ 2 ∂nu) + 2 * (b : ℝ) ^ 2 * s := by
    have hs0 : 0 < s := (sq_nonneg r).trans_lt hs
    have hcost : Transport.transportCost
        (WassersteinSpace.quadraticCost (E := E)) mu nu < ENNReal.ofReal s := by
      rw [← WassersteinSpace.wassersteinDistance_sq]
      exact hw.trans_lt ((ENNReal.ofReal_lt_ofReal_iff hs0).2 hs)
    obtain ⟨gamma, hgamma, hgammaCost⟩ :=
      Transport.exists_isCoupling_lintegral_lt_of_transportCost_lt
        (WassersteinSpace.quadraticCost (E := E)) mu nu hcost
    exact of_isCoupling hg hi hgamma hs0.le hgammaCost.le
  refine ⟨(hall (r ^ 2 + 1) (by linarith)).1, ?_⟩
  apply le_of_forall_pos_le_add
  intro epsilon hepsilon
  have hden : 0 < 2 * (b : ℝ) ^ 2 + 1 := by positivity
  have hdelta : 0 < epsilon / (2 * (b : ℝ) ^ 2 + 1) := div_pos hepsilon hden
  have hbound := (hall (r ^ 2 + epsilon / (2 * (b : ℝ) ^ 2 + 1)) (by linarith)).2
  have heq := div_mul_cancel₀ epsilon hden.ne'
  nlinarith

end

end AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinLipschitzMoment

Exact module and namespace context

Scope and omitted-condition boundaries

Ordinary quadratic Wasserstein cost only. No optimal coupling, twisted metric, probability normalization, phase history or SPHMC convergence theorem is asserted.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.integrable_toReal_of_lintegral_ne_top
MeasureTheory.integral_map
MeasureTheory.integral_mono

Mathematical sources

SPHMC Lemma D.4 prerequisite — Samplinglib-authored expansion of the standard transport step used after (D.3).

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