Samplinglib
Lean gate not recorded for this source state main · ed709a7f320d
production module

AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolation

7 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolation.lean.

Imports
AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSpace
Imported by
AutoSamplingTheory.TechnicalLemmas.MeasureAutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationCouplingAutoSamplingTheory.TechnicalLemmas.Measure.DisplacementRealQuadraticCostAutoSamplingTheory.TechnicalLemmas.Measure.QuadraticOptimalMapAutoSamplingTheory.TechnicalLemmas.Measure.QuadraticOptimalMidpointTests.DisplacementInterpolation
Placeholder scan
0 declaration(s) flagged
Gate status
Partial

Declarations

def AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolation.IsQuadraticOptimalCoupling Partial Not mapped

- 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 ed709a7f320dOpen detailed card

def AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolation.displacementInterpolation Partial Not mapped

- 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 ed709a7f320dOpen detailed card

theorem AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolation.displacementInterpolation_zero Partial Not mapped

- 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 ed709a7f320d

theorem AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolation.displacementInterpolation_one Partial Not mapped

- 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 ed709a7f320d

def AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolation.IsWassersteinGeodesic Partial Compiled

- 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 ed709a7f320dOpen detailed card

theorem AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolation.isWassersteinGeodesic_displacementInterpolation Partial Not mapped

- 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 ed709a7f320d

theorem AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolation.endpoints_of_isWassersteinGeodesic Partial Not mapped

- 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 ed709a7f320d

Complete Lean source

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolation.lean — full module with imports and context
Download module (.lean)
import AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSpace

/-!
# Displacement interpolation

This file formalizes Chewi's Definition 1.3.25 directly from an optimal
coupling measure.  It does not assume existence or uniqueness of an optimal
coupling and does not prove the constant-speed conclusion of Theorem 1.3.23.
-/

namespace AutoSamplingTheory
namespace TechnicalLemmas
namespace Measure
namespace DisplacementInterpolation

open MeasureTheory Set

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]

/-- 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 `γ`. -/
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. -/
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. -/
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. -/
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. -/
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. -/
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