ASTIS mathematical exposition

Optimal displacement interpolation has constant speed for arbitrary P2 endpoints

AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationConstantSpeed.wassersteinDistance_interpolation_eq_of_le_of_integrable_norm_sq · theorem · Teaching coverage

Statement

Let E be the repository's finite-dimensional real inner-product Borel space. Let mu0 and mu1 be probability measures with finite second moments, and let gamma be a coupling of them attaining the quadratic transport infimum. For 0 <= s <= t <= 1, the 2-Wasserstein distance between the affine pushforwards mu_s and mu_t is exactly (t-s) times the endpoint distance.

\[\mu_r=((x,y)\mapsto(1-r)x+ry)_\#\gamma,\qquad W_2(\mu_s,\mu_t)=(t-s)W_2(\mu_0,\mu_1),\qquad 0\le s\le t\le1.\]

All objects and hypotheses

E retains the existing NormedAddCommGroup, real InnerProductSpace, FiniteDimensional, Borel, SecondCountableTopology, StandardBorelSpace and Nonempty assumptions used by the interpolation and exact triangle APIs.
mu0 and mu1 are probability measures, expressed by IsProbabilityMeasure instances, and their real squared norms are integrable. Absolute continuity with respect to volume is not assumed.
gamma is supplied and is a quadratic-optimal coupling: it has marginals mu0 and mu1 and its ENNReal quadratic cost equals the transport-cost infimum. The theorem does not prove that gamma exists.
The parameters satisfy 0 <= s <= t <= 1. The ordered formula uses t-s rather than an absolute value.
The output is an equality in ENNReal. Finite second moments are used to prove that the endpoint Wasserstein distance is below infinity before additive cancellation.

Mathematical proof

1. Build probability laws along the interpolation

The optimal coupling has probability mass because its first marginal is the probability law mu0. Mapping this coupling by the measurable affine point map gives a probability measure mu_s at time s and similarly mu_t at time t. No density or absolute-continuity argument is used.

\[\mu_r=(\pi_r)_\#\gamma,\qquad \pi_r(x,y)=(1-r)x+ry,\qquad \gamma( E\times E)=1\Longrightarrow\mu_r(E)=1.\]

Corresponding Lean step

Transport.isProbabilityMeasure_of_isCoupling_left supplies the probability instance for gamma, and isProbabilityMeasure_displacementInterpolation transports it through the measurable affine map.

2. Use the canonical two-time coupling for the upper bound

Push gamma forward by the pair of affine maps at s and t. This is a coupling of mu_s and mu_t, and its displacement is exactly (t-s)(y-x). Quadratic optimality at the endpoints therefore gives the sharp upper bound for each of the three ordered subintervals [0,s], [s,t], and [t,1].

\[W_2(\mu_s,\mu_t)\le(t-s)W_2(\mu_0,\mu_1).\]

Corresponding Lean step

wassersteinDistance_interpolation_le packages the measurable two-time coupling, exact quadratic-cost scaling, endpoint optimality and monotonicity of the positive square root. Endpoint rewrites use displacementInterpolation_zero and displacementInterpolation_one.

3. Compare the three pieces with the endpoint distance

The exact Wasserstein triangle inequality along mu0, mu_s, mu_t, mu1 bounds the endpoint distance by the sum of the three segment distances. Replacing the prefix and suffix by their sharp upper bounds produces a lower bound on the middle segment after cancellation. The coefficients s, t-s and 1-t are nonnegative and sum to one.

\[W_2(\mu_0,\mu_1)\le W_2(\mu_0,\mu_s)+W_2(\mu_s,\mu_t)+W_2(\mu_t,\mu_1),\qquad s+(t-s)+(1-t)=1.\]

Corresponding Lean step

WassersteinTriangleExact.wassersteinDistance_triangle is applied twice. interpolation_coefficients_sum_one converts the coefficient partition into an ENNReal equality.

4. Justify extended-real cancellation using finite moments

Cancellation in ENNReal is invalid when the common prefix or suffix is infinite. The endpoint probability and finite-second-moment hypotheses feed the existing independent-product-coupling lemma, proving the endpoint W2 distance is finite. Multiplying by finite real coefficients keeps the prefix and suffix finite, so the two additive cancellations are sound. Combining the resulting lower bound with the canonical-coupling upper bound gives equality.

\[\int\|x\|^2\,d\mu_0<\infty,\quad\int\|y\|^2\,d\mu_1<\infty\Longrightarrow W_2(\mu_0,\mu_1)<\infty\Longrightarrow W_2(\mu_s,\mu_t)=(t-s)W_2(\mu_0,\mu_1).\]

Corresponding Lean step

WassersteinFiniteSecondMoment.wassersteinDistance_lt_top_of_integrable_norm_sq proves hd. ENNReal.mul_lt_top and ENNReal.add_le_add_iff_left/right justify the two cancellations, and le_antisymm closes the equality.

Lean statement · wassersteinDistance_interpolation_eq_of_le_of_integrable_norm_sq

The theorem quantifies over the existing ambient E, endpoint measures mu0 and mu1 with probability instances, an optimal quadratic coupling gamma, explicit Integrable squared-norm hypotheses, and ordered s,t in the unit interval. It returns the exact ENNReal Wasserstein-distance identity for the two displacementInterpolation pushforwards.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem wassersteinDistance_interpolation_eq_of_le_of_integrable_norm_sq
    {γ : Measure (E × E)} {μ₀ μ₁ : Measure E}
    [IsProbabilityMeasure μ₀] [IsProbabilityMeasure μ₁]
    (hμ₀ : Integrable (fun x : E => ‖x‖ ^ 2) μ₀)
    (hμ₁ : Integrable (fun x : E => ‖x‖ ^ 2) μ₁)
    (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 μ₀ μ₁

Exact module and namespace context

Lean proof · wassersteinDistance_interpolation_eq_of_le_of_integrable_norm_sq

The proof reuses the existing sharp interpolation upper bound and exact triangle inequality. Its only endpoint-domain change is to call wassersteinDistance_lt_top_of_integrable_norm_sq directly instead of unpacking the stronger P2ac predicate. The historical wassersteinDistance_interpolation_eq_of_le declaration and module remain unchanged. The focused compatibility test installs probability instances from its P2ac hypotheses and derives the same signature from this general theorem.

theorem wassersteinDistance_interpolation_eq_of_le_of_integrable_norm_sq
    {γ : Measure (E × E)} {μ₀ μ₁ : Measure E}
    [IsProbabilityMeasure μ₀] [IsProbabilityMeasure μ₁]
    (hμ₀ : Integrable (fun x : E => ‖x‖ ^ 2) μ₀)
    (hμ₁ : Integrable (fun x : E => ‖x‖ ^ 2) μ₁)
    (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
  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 :=
    WassersteinTriangleExact.wassersteinDistance_triangle μs μt μ₁
  have hchain :
      WassersteinSpace.wassersteinDistance μ₀ μ₁ ≤
        WassersteinSpace.wassersteinDistance μ₀ μs +
          WassersteinSpace.wassersteinDistance μs μt +
            WassersteinSpace.wassersteinDistance μt μ₁ := by
    calc
      WassersteinSpace.wassersteinDistance μ₀ μ₁ ≤
          WassersteinSpace.wassersteinDistance μ₀ μs +
            WassersteinSpace.wassersteinDistance μs μ₁ := htri_left
      _ ≤ WassersteinSpace.wassersteinDistance μ₀ μs +
            (WassersteinSpace.wassersteinDistance μs μt +
              WassersteinSpace.wassersteinDistance μt μ₁) := by
        exact add_le_add le_rfl htri_right
      _ = WassersteinSpace.wassersteinDistance μ₀ μs +
            WassersteinSpace.wassersteinDistance μs μt +
              WassersteinSpace.wassersteinDistance μt μ₁ := by
        simp [add_assoc]

  have hchain' :
      WassersteinSpace.wassersteinDistance μ₀ μ₁ ≤
        ENNReal.ofReal s * WassersteinSpace.wassersteinDistance μ₀ μ₁ +
          WassersteinSpace.wassersteinDistance μs μt +
            ENNReal.ofReal (1 - t) * WassersteinSpace.wassersteinDistance μ₀ μ₁ := by
    exact hchain.trans (add_le_add (add_le_add h0s le_rfl) ht1')

  have hcoeff := interpolation_coefficients_sum_one hs0 hst ht1
  have hpartition :
      WassersteinSpace.wassersteinDistance μ₀ μ₁ =
        ENNReal.ofReal s * WassersteinSpace.wassersteinDistance μ₀ μ₁ +
          ENNReal.ofReal (t - s) * WassersteinSpace.wassersteinDistance μ₀ μ₁ +
            ENNReal.ofReal (1 - t) * WassersteinSpace.wassersteinDistance μ₀ μ₁ := by
    calc
      WassersteinSpace.wassersteinDistance μ₀ μ₁ =
          1 * WassersteinSpace.wassersteinDistance μ₀ μ₁ := by simp
      _ = (ENNReal.ofReal s + ENNReal.ofReal (t - s) + ENNReal.ofReal (1 - t)) *
            WassersteinSpace.wassersteinDistance μ₀ μ₁ := by rw [hcoeff]
      _ = ENNReal.ofReal s * WassersteinSpace.wassersteinDistance μ₀ μ₁ +
            ENNReal.ofReal (t - s) * WassersteinSpace.wassersteinDistance μ₀ μ₁ +
              ENNReal.ofReal (1 - t) * WassersteinSpace.wassersteinDistance μ₀ μ₁ := by
        simp [add_mul, add_assoc]

  have hcancelInput :
      ENNReal.ofReal s * WassersteinSpace.wassersteinDistance μ₀ μ₁ +
          ENNReal.ofReal (t - s) * WassersteinSpace.wassersteinDistance μ₀ μ₁ +
            ENNReal.ofReal (1 - t) * WassersteinSpace.wassersteinDistance μ₀ μ₁ ≤
        ENNReal.ofReal s * WassersteinSpace.wassersteinDistance μ₀ μ₁ +
          WassersteinSpace.wassersteinDistance μs μt +
            ENNReal.ofReal (1 - t) * WassersteinSpace.wassersteinDistance μ₀ μ₁ := by
    rw [← hpartition]
    exact hchain'

  have hd : WassersteinSpace.wassersteinDistance μ₀ μ₁ < ∞ :=
    WassersteinFiniteSecondMoment.wassersteinDistance_lt_top_of_integrable_norm_sq
      μ₀ μ₁ hμ₀ hμ₁
  have hprefix :
      ENNReal.ofReal s * WassersteinSpace.wassersteinDistance μ₀ μ₁ < ∞ :=
    ENNReal.mul_lt_top ENNReal.ofReal_lt_top hd
  have hsuffix :
      ENNReal.ofReal (1 - t) * WassersteinSpace.wassersteinDistance μ₀ μ₁ < ∞ :=
    ENNReal.mul_lt_top ENNReal.ofReal_lt_top hd

  have hcancelSuffix :
      ENNReal.ofReal s * WassersteinSpace.wassersteinDistance μ₀ μ₁ +
          ENNReal.ofReal (t - s) * WassersteinSpace.wassersteinDistance μ₀ μ₁ ≤
        ENNReal.ofReal s * WassersteinSpace.wassersteinDistance μ₀ μ₁ +
          WassersteinSpace.wassersteinDistance μs μt := by
    exact (ENNReal.add_le_add_iff_right hsuffix.ne).mp
      (by simpa [add_assoc] using hcancelInput)
  have hlower :
      ENNReal.ofReal (t - s) * WassersteinSpace.wassersteinDistance μ₀ μ₁ ≤
        WassersteinSpace.wassersteinDistance μs μt :=
    (ENNReal.add_le_add_iff_left hprefix.ne).mp hcancelSuffix

  change WassersteinSpace.wassersteinDistance μs μt =
    ENNReal.ofReal (t - s) * WassersteinSpace.wassersteinDistance μ₀ μ₁
  exact le_antisymm hupper hlower

end

end DisplacementInterpolationConstantSpeed
end Measure
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

Scope and omitted-condition boundaries

This is exactly the ordered metric-identity component of Statistical Optimal Transport Theorem 7.6, conditional on a supplied optimal plan; it does not prove optimal-plan existence or the complete geodesic-space assertion.
Relative to Log-Concave Sampling Theorem 1.3.23, removing endpoint absolute continuity is a genuine generalization. That source's P2ac theorem and IsWassersteinGeodesic interface remain unchanged and follow as a compatibility corollary.
No uniqueness, continuity equation, Benamou-Brenier identity, optimal map, path continuity, arbitrary-time symmetry wrapper, or completion of either source chapter is claimed.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

ENNReal.mul_lt_top
ENNReal.add_le_add_iff_left
ENNReal.add_le_add_iff_right
le_antisymm

Mathematical sources

Chewi, Niles-Weed and Rigollet, Statistical Optimal Transport, Theorem 7.6, printed pp.209-210/PDF pp.215-216 — Direct source for arbitrary P2 endpoints, the optimal-plan affine pushforward and the constant-speed identity. ASTIS formalizes only the ordered metric identity conditional on the plan.
Chewi, Log-Concave Sampling, Theorem 1.3.23 and Definition 1.3.25, printed p.30/PDF p.42 — The existing P2ac source theorem is the compatibility specialization. It is not the source for removing absolute continuity.

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.