Samplinglib mathematical lesson

M-kappa transport controls ordinary phase transport

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

Read this first

Mathematical statement

Ordinary squared Wasserstein distance is at most six times the M-kappa squared transport value.

\[W_2^2(\mu,\nu)\le6W_{2,M_\kappa}^2(\mu,\nu).\]

Lean statement · wassersteinDistance_sq_le_phaseWassersteinSq

The ENNReal conclusion includes infinite-cost laws without a separate branch in the statement.

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 wassersteinDistance_sq_le_phaseWassersteinSq
    [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
    {kappa : ℝ} (hkappa : 1 ≤ kappa) (mu nu : Measure (E × E)) :
    WassersteinSpace.wassersteinDistance mu nu ^ 2 ≤
      ENNReal.ofReal 6 * phaseWassersteinSq kappa mu nu

Exact module and namespace context

Proof roadmap

1Lower-bound the twisted form
Cauchy--Schwarz and a completed square absorb the cross term without losing kappa.
2Compare each coupling
The product max norm is bounded by the Euclidean sum of coordinate squares.
3Remove near-optimal excess
Choose a twisted coupling within delta of the infimum and let delta vanish; no optimizer is assumed.

Full assumptions and notation

All objects and hypotheses

kappa≥1.
The two laws are arbitrary measures on phase space.

Mathematical proof

1. Lower-bound the twisted form

Cauchy--Schwarz and a completed square absorb the cross term without losing kappa.

\[q_\kappa(x,p)\ge\frac16(\|x\|^2+\|p\|^2).\]

Corresponding Lean step

Private ordinary_energy_le_phaseQuadraticForm.

2. Compare each coupling

The product max norm is bounded by the Euclidean sum of coordinate squares.

\[\|z-z'\|_{\max}^2\le6q_\kappa(z-z').\]

Corresponding Lean step

lintegral_mono and lintegral_const_mul.

3. Remove near-optimal excess

Choose a twisted coupling within delta of the infimum and let delta vanish; no optimizer is assumed.

\[\forall\varepsilon>0,\ W_2^2\le6W_{2,M_\kappa}^2+\varepsilon.\]

Corresponding Lean step

exists_isCoupling_lintegral_lt_of_transportCost_lt and ENNReal.le_of_forall_pos_le_add.

Lean verification

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

Lean proof · wassersteinDistance_sq_le_phaseWassersteinSq

Pointwise quadratic comparison, monotone integration, near-optimal coupling, epsilon closure.

Download module (.lean)

theorem wassersteinDistance_sq_le_phaseWassersteinSq
    [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
    {kappa : ℝ} (hkappa : 1 ≤ kappa) (mu nu : Measure (E × E)) :
    WassersteinSpace.wassersteinDistance mu nu ^ 2 ≤
      ENNReal.ofReal 6 * phaseWassersteinSq kappa mu nu := by
  rw [WassersteinSpace.wassersteinDistance_sq]
  apply ENNReal.le_of_forall_pos_le_add
  intro epsilon hepsilon hfinite
  let A : ℝ≥0∞ := ENNReal.ofReal 6
  let C : ℝ≥0∞ := phaseWassersteinSq kappa mu nu
  have hA0 : A ≠ 0 := by
    simp [A]
  have hAtop : A ≠ ⊤ := ENNReal.ofReal_ne_top
  have hCtop : C < ⊤ := by
    rcases ENNReal.mul_lt_top_iff.mp hfinite with h | h | h
    · exact h.2
    · exact (hA0 h).elim
    · simpa [C, h]
  let delta : ℝ≥0∞ := (epsilon : ℝ≥0∞) / A
  have hdelta0 : delta ≠ 0 := by
    have hepsilon0 : (epsilon : ℝ≥0∞) ≠ 0 := by exact_mod_cast hepsilon.ne'
    exact (ENNReal.div_pos hepsilon0 hAtop).ne'
  have hstrict : C < C + delta :=
    ENNReal.lt_add_right hCtop.ne hdelta0
  obtain ⟨gamma, hgamma, hgammaCost⟩ :=
    Transport.exists_isCoupling_lintegral_lt_of_transportCost_lt
      (phaseCost (E := E) kappa) mu nu hstrict
  have hphaseMeas : Measurable (phaseCost (E := E) kappa) := by
    unfold phaseCost phaseQuadraticForm
    fun_prop
  calc
    Transport.transportCost (WassersteinSpace.quadraticCost (E := E × E)) mu nu ≤
        ∫⁻ z, WassersteinSpace.quadraticCost (E := E × E) z ∂gamma :=
      Transport.transportCost_le_lintegral_of_isCoupling _ mu nu gamma hgamma
    _ ≤ ∫⁻ z, A * phaseCost (E := E) kappa z ∂gamma := by
      apply lintegral_mono
      intro z
      exact quadraticCost_le_phaseCost hkappa z
    _ = A * ∫⁻ z, phaseCost (E := E) kappa z ∂gamma := by
      exact lintegral_const_mul _ hphaseMeas
    _ ≤ A * (C + delta) := by
      gcongr
    _ = A * C + (epsilon : ℝ≥0∞) := by
      rw [mul_add, show A * delta = (epsilon : ℝ≥0∞) by
        exact ENNReal.mul_div_cancel hA0 hAtop]
    _ = ENNReal.ofReal 6 * phaseWassersteinSq kappa mu nu +
        (epsilon : ℝ≥0∞) := rfl

Exact module and namespace context

Scope and omitted-condition boundaries

One-way comparison with explicit kappa-uniform factor 6; no contraction or (D.3).

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

abs_real_inner_le_norm
ENNReal.le_of_forall_pos_le_add

Mathematical sources

Uniform norm equivalence after M-kappa definition — ASTIS expands the omitted constants and infimum argument.

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