production module

`AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSpace`

5 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Measure/WassersteinSpace.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Measure.TransportMathlib.Analysis.SpecialFunctions.Pow.NNReal externalMathlib.MeasureTheory.Measure.Haar.InnerProductSpace externalMathlib.MeasureTheory.Integral.Bochner.Basic external

Imported by

AutoSamplingTheory.TechnicalLemmas.MeasureAutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationTests.WassersteinSpace

Placeholder scan

0 declaration(s) flagged

Gate status

Compiled

Declarations

def AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSpace.quadraticCost Compiled Not mapped

- Squared Euclidean transport cost as an extended nonnegative function.

def quadraticCost
    {E : Type*} [NormedAddCommGroup E] : E × E → ℝ≥0∞ :=
  fun z => ENNReal.ofReal (‖z.1 - z.2‖ ^ 2)

/-- Chewi Definition 1.3.4: the 2-Wasserstein distance is the positive
square root of the quadratic Kantorovich transport cost. -/

AutoSamplingTheory/TechnicalLemmas/Measure/WassersteinSpace.lean:23published source at 7bcd37294df1

def AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSpace.wassersteinDistance Compiled Compiled

- Chewi Definition 1.3.4: the 2-Wasserstein distance is the positive square root of the quadratic Kantorovich transport cost.

noncomputable def wassersteinDistance
    {E : Type*} [NormedAddCommGroup E] [MeasurableSpace E]
    (μ ν : Measure E) : ℝ≥0∞ :=
  (Transport.transportCost (quadraticCost (E := E)) μ ν) ^ (1 / 2 : ℝ)

/-- Chewi display (1.3.5): the square of `W₂` is the infimum of the
quadratic costs over all couplings. -/

AutoSamplingTheory/TechnicalLemmas/Measure/WassersteinSpace.lean:29published source at 7bcd37294df1Open detailed card

theorem AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSpace.wassersteinDistance_sq Compiled Compiled

- Chewi display (1.3.5): the square of `W₂` is the infimum of the quadratic costs over all couplings.

theorem wassersteinDistance_sq
    {E : Type*} [NormedAddCommGroup E] [MeasurableSpace E]
    (μ ν : Measure E) :
    wassersteinDistance μ ν ^ 2 =
      Transport.transportCost (quadraticCost (E := E)) μ ν := by
  rw [wassersteinDistance, ← ENNReal.rpow_two, ← ENNReal.rpow_mul]
  norm_num

/-- Chewi Definition 1.3.12: a probability measure in `P₂,ac` has finite
second moment and is absolutely continuous with respect to Lebesgue volume.

The generic finite-dimensional real inner-product space specializes to
Euclidean `R^d` in the source. -/

AutoSamplingTheory/TechnicalLemmas/Measure/WassersteinSpace.lean:36published source at 7bcd37294df1Open detailed card

def AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSpace.IsAbsolutelyContinuousFiniteSecondMoment Compiled Compiled

- Chewi Definition 1.3.12: a probability measure in `P₂,ac` has finite second moment and is absolutely continuous with respect to Lebesgue volume. The generic finite-dimensional real inner-product space specializes to Euclidean `R^d` in the source.

def IsAbsolutelyContinuousFiniteSecondMoment
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (μ : Measure E) : Prop :=
  IsProbabilityMeasure μ ∧
    μ ≪ (volume : Measure E) ∧
    Integrable (fun x : E => ‖x‖ ^ 2) μ

/-- Expansion of the three conditions in the `P₂,ac` definition. -/

AutoSamplingTheory/TechnicalLemmas/Measure/WassersteinSpace.lean:49published source at 7bcd37294df1Open detailed card

theorem AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSpace.isAbsolutelyContinuousFiniteSecondMoment_iff Compiled Not mapped

- Expansion of the three conditions in the `P₂,ac` definition.

theorem isAbsolutelyContinuousFiniteSecondMoment_iff
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (μ : Measure E) :
    IsAbsolutelyContinuousFiniteSecondMoment μ ↔
      IsProbabilityMeasure μ ∧
        μ ≪ (volume : Measure E) ∧
        Integrable (fun x : E => ‖x‖ ^ 2) μ :=
  Iff.rfl

end WassersteinSpace
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/WassersteinSpace.lean:58published source at 7bcd37294df1