AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolation

- A coupling is quadratic-cost optimal when it attains the Kantorovich infimum defining the squared 2-Wasserstein distance.

def IsQuadraticOptimalCoupling
    (γ : Measure (E × E)) (μ₀ μ₁ : Measure E) : Prop :=
  Transport.IsCoupling γ μ₀ μ₁ ∧
    (∫⁻ z, WassersteinSpace.quadraticCost z ∂γ) =
      Transport.transportCost WassersteinSpace.quadraticCost μ₀ μ₁

/-- The law at time `t` of `(1 - t) X₀ + t X₁` when the joint law of
`(X₀, X₁)` is `γ`. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolation.lean:23published source at 7bcd37294df1Open detailed card

- The law at time `t` of `(1 - t) X₀ + t X₁` when the joint law of `(X₀, X₁)` is `γ`.

noncomputable def displacementInterpolation
    (γ : Measure (E × E)) (t : ℝ) : Measure E :=
  γ.map fun z => (1 - t) • z.1 + t • z.2

omit [FiniteDimensional ℝ E] [BorelSpace E] in
/-- The displacement interpolation starts at the first marginal. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolation.lean:31published source at 7bcd37294df1Open detailed card

- The displacement interpolation starts at the first marginal.

theorem displacementInterpolation_zero
    {γ : Measure (E × E)} {μ₀ μ₁ : Measure E}
    (hγ : Transport.IsCoupling γ μ₀ μ₁) :
    displacementInterpolation γ 0 = μ₀ := by
  simpa [displacementInterpolation, Measure.fst] using hγ.1

omit [FiniteDimensional ℝ E] [BorelSpace E] in
/-- The displacement interpolation ends at the second marginal. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolation.lean:37published source at 7bcd37294df1

- The displacement interpolation ends at the second marginal.

theorem displacementInterpolation_one
    {γ : Measure (E × E)} {μ₀ μ₁ : Measure E}
    (hγ : Transport.IsCoupling γ μ₀ μ₁) :
    displacementInterpolation γ 1 = μ₁ := by
  simpa [displacementInterpolation, Measure.snd] using hγ.2

/-- Chewi Definition 1.3.25: a Wasserstein geodesic, also called the
displacement or McCann interpolation, is the affine-law curve generated by
an optimal coupling of two `P₂,ac` endpoint laws.

The name records the source definition.  The metric constant-speed property
and uniqueness are the content of Theorem 1.3.23 and remain separate. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolation.lean:45published source at 7bcd37294df1

- Chewi Definition 1.3.25: a Wasserstein geodesic, also called the displacement or McCann interpolation, is the affine-law curve generated by an optimal coupling of two `P₂,ac` endpoint laws. The name records the source definition. The metric constant-speed property and uniqueness are the content of Theorem 1.3.23 and remain separate.

def IsWassersteinGeodesic
    (μ₀ μ₁ : Measure E) (curve : ℝ → Measure E) : Prop :=
  WassersteinSpace.IsAbsolutelyContinuousFiniteSecondMoment μ₀ ∧
    WassersteinSpace.IsAbsolutelyContinuousFiniteSecondMoment μ₁ ∧
    ∃ γ : Measure (E × E),
      IsQuadraticOptimalCoupling γ μ₀ μ₁ ∧
      ∀ t ∈ Icc (0 : ℝ) 1,
        curve t = displacementInterpolation γ t

/-- An optimal coupling and two `P₂,ac` endpoints generate the source
displacement-interpolation predicate. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolation.lean:57published source at 7bcd37294df1Open detailed card

- An optimal coupling and two `P₂,ac` endpoints generate the source displacement-interpolation predicate.

theorem isWassersteinGeodesic_displacementInterpolation
    {γ : Measure (E × E)} {μ₀ μ₁ : Measure E}
    (hμ₀ : WassersteinSpace.IsAbsolutelyContinuousFiniteSecondMoment μ₀)
    (hμ₁ : WassersteinSpace.IsAbsolutelyContinuousFiniteSecondMoment μ₁)
    (hγ : IsQuadraticOptimalCoupling γ μ₀ μ₁) :
    IsWassersteinGeodesic μ₀ μ₁ (displacementInterpolation γ) := by
  exact ⟨hμ₀, hμ₁, γ, hγ, fun _ _ => rfl⟩

/-- Every source displacement interpolation has the prescribed endpoints. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolation.lean:68published source at 7bcd37294df1

- Every source displacement interpolation has the prescribed endpoints.

theorem endpoints_of_isWassersteinGeodesic
    {μ₀ μ₁ : Measure E} {curve : ℝ → Measure E}
    (hcurve : IsWassersteinGeodesic μ₀ μ₁ curve) :
    curve 0 = μ₀ ∧ curve 1 = μ₁ := by
  rcases hcurve.2.2 with ⟨γ, hγ, hcurve⟩
  constructor
  · rw [hcurve 0 (by simp)]
    exact displacementInterpolation_zero hγ.1
  · rw [hcurve 1 (by simp)]
    exact displacementInterpolation_one hγ.1

end DisplacementInterpolation
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolation.lean:77published source at 7bcd37294df1