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

Squared Wasserstein cost in the M-kappa geometry

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseMetric.phaseWassersteinSq · def · Teaching coverage

Read this first

Mathematical statement

Take the infimum of the exact M-kappa cost over all couplings.

\[W_{2,M_\kappa}^2(\mu,\nu)=\inf_{\gamma\in\Gamma(\mu,\nu)}\int c_\kappa\,d\gamma.\]
Lean statement · phaseWassersteinSq

The value is ENNReal and therefore retains infinite costs.

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)
def phaseWassersteinSq [MeasurableSpace E] (kappa : ℝ)
    (mu nu : Measure (E × E)) : ℝ≥0∞

Exact module and namespace context

Proof roadmap

  1. 1Reuse the canonical transport infimum

    No second Wasserstein implementation is introduced.

Full assumptions and notation

All objects and hypotheses

  • The phase space carries the product measurable structure.

Construction and meaning

1. Reuse the canonical transport infimum

No second Wasserstein implementation is introduced.

\[W_{2,M_\kappa}^2=\mathsf{transportCost}(c_\kappa).\]
Corresponding Lean step

Transport.transportCost.

Lean verification

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

Lean construction · phaseWassersteinSq

Definition by the shared Kantorovich API.

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)
def phaseWassersteinSq [MeasurableSpace E] (kappa : ℝ)
    (mu nu : Measure (E × E)) : ℝ≥0∞ :=
  Transport.transportCost (phaseCost (E := E) kappa) mu nu

Exact module and namespace context

Scope and omitted-condition boundaries
  • Raw Kantorovich infimum; optimizer existence is not included.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

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.