AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationConstantSpeed

- A displacement marginal of a probability coupling is again a probability measure.

theorem isProbabilityMeasure_displacementInterpolation
    {γ : Measure (E × E)} {μ₀ μ₁ : Measure E}
    [IsProbabilityMeasure μ₀]
    (hγ : Transport.IsCoupling γ μ₀ μ₁) (t : ℝ) :
    IsProbabilityMeasure (displacementInterpolation γ t) := by
  letI : IsProbabilityMeasure γ :=
    Transport.isProbabilityMeasure_of_isCoupling_left hγ
  unfold displacementInterpolation
  exact Measure.isProbabilityMeasure_map (measurable_pointMap (E := E) t).aemeasurable

/-- The canonical two-time interpolation coupling gives the sharp linear upper
bound when the times are ordered. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolationConstantSpeed.lean:37published source at 0e31a3cda412

- The canonical two-time interpolation coupling gives the sharp linear upper bound when the times are ordered.

theorem wassersteinDistance_interpolation_le
    {γ : Measure (E × E)} {μ₀ μ₁ : Measure E}
    (hγ : IsQuadraticOptimalCoupling γ μ₀ μ₁)
    {s t : ℝ} (hst : s ≤ t) :
    WassersteinSpace.wassersteinDistance
        (displacementInterpolation γ s)
        (displacementInterpolation γ t) ≤
      ENNReal.ofReal (t - s) *
        WassersteinSpace.wassersteinDistance μ₀ μ₁ := by
  have hsquare :=
    DisplacementInterpolationCost.wassersteinDistance_sq_interpolation_le
      (E := E) γ s t
  rw [hγ.2, ← WassersteinSpace.wassersteinDistance_sq] at hsquare
  have habs : |s - t| = t - s := by
    rw [abs_sub_comm, abs_of_nonneg (sub_nonneg.mpr hst)]
  rw [habs, ENNReal.ofReal_pow (sub_nonneg.mpr hst) 2, ← mul_pow] at hsquare
  have hsquare' :
      WassersteinSpace.wassersteinDistance
          (displacementInterpolation γ s)
          (displacementInterpolation γ t) ^ (2 : ℝ) ≤
        (ENNReal.ofReal (t - s) *
          WassersteinSpace.wassersteinDistance μ₀ μ₁) ^ (2 : ℝ) := by
    simpa [ENNReal.rpow_two] using hsquare
  exact (ENNReal.rpow_le_rpow_iff (by norm_num : (0 : ℝ) < 2)).mp hsquare'

/-- Ordered times partition the unit interval into the three nonnegative pieces
`s`, `t-s`, and `1-t`. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolationConstantSpeed.lean:49published source at 0e31a3cda412

- Ordered times partition the unit interval into the three nonnegative pieces `s`, `t-s`, and `1-t`.

theorem interpolation_coefficients_sum_one
    {s t : ℝ} (hs0 : 0 ≤ s) (hst : s ≤ t) (ht1 : t ≤ 1) :
    ENNReal.ofReal s + ENNReal.ofReal (t - s) + ENNReal.ofReal (1 - t) = 1 := by
  have hts0 : 0 ≤ t - s := sub_nonneg.mpr hst
  have h1t0 : 0 ≤ 1 - t := sub_nonneg.mpr ht1
  rw [← ENNReal.ofReal_add hs0 hts0]
  rw [← ENNReal.ofReal_add (add_nonneg hs0 hts0) h1t0]
  norm_num

/-- Chewi's constant-speed identity for ordered interpolation times.

The endpoint laws carry the source `P₂,ac` assumptions.  Absolute continuity
is not used in the metric argument itself; its role here is to keep the theorem
aligned with the source geodesic predicate, while finite second moments provide
the exact `W₂ < ∞` fact needed for cancellation. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolationConstantSpeed.lean:76published source at 0e31a3cda412

- Chewi's constant-speed identity for ordered interpolation times. The endpoint laws carry the source `P₂,ac` assumptions. Absolute continuity is not used in the metric argument itself; its role here is to keep the theorem aligned with the source geodesic predicate, while finite second moments provide the exact `W₂ < ∞` fact needed for cancellation.

theorem wassersteinDistance_interpolation_eq_of_le
    {γ : Measure (E × E)} {μ₀ μ₁ : Measure E}
    (hμ₀ : WassersteinSpace.IsAbsolutelyContinuousFiniteSecondMoment μ₀)
    (hμ₁ : WassersteinSpace.IsAbsolutelyContinuousFiniteSecondMoment μ₁)
    (hγ : IsQuadraticOptimalCoupling γ μ₀ μ₁)
    {s t : ℝ} (hs0 : 0 ≤ s) (hst : s ≤ t) (ht1 : t ≤ 1) :
    WassersteinSpace.wassersteinDistance
        (displacementInterpolation γ s)
        (displacementInterpolation γ t) =
      ENNReal.ofReal (t - s) *
        WassersteinSpace.wassersteinDistance μ₀ μ₁ := by
  letI : IsProbabilityMeasure μ₀ := hμ₀.1
  letI : IsProbabilityMeasure μ₁ := hμ₁.1
  let μs : Measure E := displacementInterpolation γ s
  let μt : Measure E := displacementInterpolation γ t
  letI : IsProbabilityMeasure μs := by
    dsimp [μs]
    exact isProbabilityMeasure_displacementInterpolation hγ.1 s
  letI : IsProbabilityMeasure μt := by
    dsimp [μt]
    exact isProbabilityMeasure_displacementInterpolation hγ.1 t

  have hupper :
      WassersteinSpace.wassersteinDistance μs μt ≤
        ENNReal.ofReal (t - s) * WassersteinSpace.wassersteinDistance μ₀ μ₁ := by
    simpa [μs, μt] using wassersteinDistance_interpolation_le (E := E) hγ hst

  have h0s :
      WassersteinSpace.wassersteinDistance μ₀ μs ≤
        ENNReal.ofReal s * WassersteinSpace.wassersteinDistance μ₀ μ₁ := by
    have h := wassersteinDistance_interpolation_le (E := E) hγ hs0
    rw [displacementInterpolation_zero hγ.1] at h
    simpa [μs] using h

  have ht1' :
      WassersteinSpace.wassersteinDistance μt μ₁ ≤
        ENNReal.ofReal (1 - t) * WassersteinSpace.wassersteinDistance μ₀ μ₁ := by
    have h := wassersteinDistance_interpolation_le (E := E) hγ ht1
    rw [displacementInterpolation_one hγ.1] at h
    simpa [μt] using h

  have htri_left :=
    WassersteinTriangleExact.wassersteinDistance_triangle μ₀ μs μ₁
  have htri_right :=
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolationConstantSpeed.lean:91published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.