production module

`AutoSamplingTheory.TechnicalLemmas.Measure.ChewiTheorem1_3_23`

2 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Measure/ChewiTheorem1_3_23.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationConstantSpeedAutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSymmetry

Imported by

AutoSamplingTheory.TechnicalLemmas.MeasureTests.ChewiTheorem1_3_23

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

theorem AutoSamplingTheory.TechnicalLemmas.Measure.ChewiTheorem1_3_23.wassersteinDistance_displacementInterpolation_eq_abs Partial Not mapped

- Arbitrary-time form of the constant-speed identity for the displacement interpolation generated by one quadratic-optimal coupling.

theorem wassersteinDistance_displacementInterpolation_eq_abs
    {γ : Measure (E × E)} {μ₀ μ₁ : Measure E}
    (hμ₀ : WassersteinSpace.IsAbsolutelyContinuousFiniteSecondMoment μ₀)
    (hμ₁ : WassersteinSpace.IsAbsolutelyContinuousFiniteSecondMoment μ₁)
    (hγ : IsQuadraticOptimalCoupling γ μ₀ μ₁)
    {s t : ℝ} (hs : s ∈ Icc (0 : ℝ) 1) (ht : t ∈ Icc (0 : ℝ) 1) :
    WassersteinSpace.wassersteinDistance
        (displacementInterpolation γ s)
        (displacementInterpolation γ t) =
      ENNReal.ofReal |s - t| *
        WassersteinSpace.wassersteinDistance μ₀ μ₁ := by
  rcases le_total s t with hst | hts
  · have h :=
      DisplacementInterpolationConstantSpeed.wassersteinDistance_interpolation_eq_of_le
        (E := E) hμ₀ hμ₁ hγ hs.1 hst ht.2
    have habs : |s - t| = t - s := by
      rw [abs_sub_comm, abs_of_nonneg (sub_nonneg.mpr hst)]
    simpa [habs] using h
  · have h :=
      DisplacementInterpolationConstantSpeed.wassersteinDistance_interpolation_eq_of_le
        (E := E) hμ₀ hμ₁ hγ ht.1 hts hs.2
    calc
      WassersteinSpace.wassersteinDistance
          (displacementInterpolation γ s)
          (displacementInterpolation γ t) =
        WassersteinSpace.wassersteinDistance
          (displacementInterpolation γ t)
          (displacementInterpolation γ s) :=
        WassersteinSymmetry.wassersteinDistance_comm _ _
      _ = ENNReal.ofReal (s - t) *
          WassersteinSpace.wassersteinDistance μ₀ μ₁ := h
      _ = ENNReal.ofReal |s - t| *
          WassersteinSpace.wassersteinDistance μ₀ μ₁ := by
        rw [abs_of_nonneg (sub_nonneg.mpr hts)]

/-- Chewi Theorem 1.3.23 in the repository's source-side geodesic interface:
any curve represented by an optimal displacement interpolation has constant
`W₂` speed on `[0,1]`. -/

AutoSamplingTheory/TechnicalLemmas/Measure/ChewiTheorem1_3_23.lean:44published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.ChewiTheorem1_3_23.chewi_theorem_1_3_23_constant_speed Partial Not mapped

- Chewi Theorem 1.3.23 in the repository's source-side geodesic interface: any curve represented by an optimal displacement interpolation has constant `W₂` speed on `[0,1]`.

theorem chewi_theorem_1_3_23_constant_speed
    {μ₀ μ₁ : Measure E} {curve : ℝ → Measure E}
    (hcurve : IsWassersteinGeodesic μ₀ μ₁ curve)
    {s t : ℝ} (hs : s ∈ Icc (0 : ℝ) 1) (ht : t ∈ Icc (0 : ℝ) 1) :
    WassersteinSpace.wassersteinDistance (curve s) (curve t) =
      ENNReal.ofReal |s - t| *
        WassersteinSpace.wassersteinDistance μ₀ μ₁ := by
  rcases hcurve with ⟨hμ₀, hμ₁, γ, hγ, hrepr⟩
  rw [hrepr s hs, hrepr t ht]
  exact wassersteinDistance_displacementInterpolation_eq_abs
    (E := E) hμ₀ hμ₁ hγ hs ht

end

end ChewiTheorem1_3_23
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/ChewiTheorem1_3_23.lean:82published source at 0e31a3cda412