Optimal transport and Wasserstein geometry

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremBrenier's theorem #

Let μ and ν be probability measures on a finite-dimensional real inner product space E, with μ absolutely continuous with respect to an additive Haar measure, and suppose the optimal cost for ‖x - y‖ ^ 2 / 2 is finite, as it is for laws with finite second moment (TauCeti.transportCost_norm_sub_sq_div_two_ne_top). Then there is a convex, lower semicontinuous u : E → EReal that never takes the value ⊥, is finite near μ-almost every point and has differentiable real representative there, such that the gradient T = ∇ (fun x => (u x).toReal):

is an optimal transport map from μ to ν, attaining the Kantorovich value;
induces the unique optimal plan: a plan is optimal exactly when it is the graph plan of T;
is the unique optimal transport map up to μ-almost everywhere equality.

TauCeti.exists_isKantorovichOptimalTransportMap_gradient.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  {ρ : MeasureTheory.Measure E} [ρ.IsAddHaarMeasure] {μ ν : MeasureTheory.Measure E}
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν]
  (hμ : μ.AbsolutelyContinuous ρ)
  (hfin : TauCeti.transportCost (fun z => ENNReal.ofReal (‖z.1 - z.2‖ ^ 2 / 2)) μ ν ≠ ⊤) :
  ∃ u,
    Convex ℝ {p | u p.1 ≤ ↑p.2} ∧
      LowerSemicontinuous u ∧
        (∀ (x : E), u x ≠ ⊥) ∧
          (∀ᵐ (x : E) ∂μ,
              (∀ᶠ (x' : E) in nhds x, u x' ≠ ⊤) ∧ DifferentiableAt ℝ (fun x' => (u x').toReal) x) ∧
            TauCeti.IsKantorovichOptimalTransportMap (fun z => ENNReal.ofReal (‖z.1 - z.2‖ ^ 2 / 2))
                μ ν (gradient fun x => (u x).toReal) ∧
              (∀ (π : MeasureTheory.Measure (E × E)),
                  TauCeti.IsOptimalCoupling (fun z => ENNReal.ofReal (‖z.1 - z.2‖ ^ 2 / 2)) π μ ν ↔
                    π = TauCeti.graphPlan (gradient fun x => (u x).toReal) μ) ∧
                ∀ (S : E → E),
                  TauCeti.IsKantorovichOptimalTransportMap
                      (fun z => ENNReal.ofReal (‖z.1 - z.2‖ ^ 2 / 2)) μ ν S →
                    S =ᵐ[μ] gradient fun x => (u x).toReal

Lean

Formalized in Tau Ceti as TauCeti.exists_isKantorovichOptimalTransportMap_gradient.

Other forms

Brenier's theorem for the cost edist ^ 2. Formalized in Tau Ceti as TauCeti.IsOptimalCoupling.exists_eq_graphPlan_of_absolutelyContinuous.

TauCeti.IsOptimalCoupling.exists_eq_graphPlan_of_absolutelyContinuous.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
  [BorelSpace E] {ρ : MeasureTheory.Measure E} [ρ.IsAddHaarMeasure] {μ ν : MeasureTheory.Measure E}
  [MeasureTheory.IsFiniteMeasure μ] {π : MeasureTheory.Measure (E × E)}
  (hμ : μ.AbsolutelyContinuous ρ) (h : TauCeti.IsOptimalCoupling (fun z => edist z.1 z.2 ^ 2) π μ ν)
  (hfin : TauCeti.wassersteinEDist 2 μ ν ≠ ⊤) : ∃ T, Measurable T ∧ π = TauCeti.graphPlan T μ

Brenier's theorem with the inverse map. Formalized in Tau Ceti as TauCeti.exists_isKantorovichOptimalTransportMap_gradient_and_gradient_fenchelConjugate.

TauCeti.exists_isKantorovichOptimalTransportMap_gradient_and_gradient_fenchelConjugate.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] {ρ : MeasureTheory.Measure E} [ρ.IsAddHaarMeasure]
  {μ ν : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.IsProbabilityMeasure ν] (hμ : μ.AbsolutelyContinuous ρ)
  (hν : ν.AbsolutelyContinuous ρ)
  (hfin : TauCeti.transportCost (fun z => ENNReal.ofReal (‖z.1 - z.2‖ ^ 2 / 2)) μ ν ≠ ⊤) :
  ∃ u,
    Convex ℝ {p | u p.1 ≤ ↑p.2} ∧
      LowerSemicontinuous u ∧
        (∀ (x : E), u x ≠ ⊥) ∧
          (∀ᵐ (x : E) ∂μ,
              (∀ᶠ (x' : E) in nhds x, u x' ≠ ⊤) ∧ DifferentiableAt ℝ (fun x' => (u x').toReal) x) ∧
            (∀ᵐ (y : E) ∂ν,
                (∀ᶠ (y' : E) in nhds y, TauCeti.fenchelConjugate (innerₗ E) u y' ≠ ⊤) ∧
                  DifferentiableAt ℝ (fun y' => (TauCeti.fenchelConjugate (innerₗ E) u y').toReal)
                    y) ∧
              TauCeti.IsKantorovichOptimalTransportMap
                  (fun z => ENNReal.ofReal (‖z.1 - z.2‖ ^ 2 / 2)) μ ν
                  (gradient fun x => (u x).toReal) ∧
                TauCeti.IsKantorovichOptimalTransportMap
                    (fun z => ENNReal.ofReal (‖z.1 - z.2‖ ^ 2 / 2)) ν μ
                    (gradient fun y => (TauCeti.fenchelConjugate (innerₗ E) u y).toReal) ∧
                  ((gradient fun y => (TauCeti.fenchelConjugate (innerₗ E) u y).toReal) ∘
                        gradient fun x => (u x).toReal) =ᵐ[μ]
                      id ∧
                    ((gradient fun x => (u x).toReal) ∘
                        gradient fun y => (TauCeti.fenchelConjugate (innerₗ E) u y).toReal) =ᵐ[ν]
                      id

Sources

LeanTauCeti.exists_isKantorovichOptimalTransportMap_gradient · TauCeti.IsOptimalCoupling.exists_eq_graphPlan_of_absolutelyContinuous · TauCeti.exists_isKantorovichOptimalTransportMap_gradient_and_gradient_fenchelConjugate

Uses 3

Proof usesThe Fenchel–Young inequality · Rademacher's theorem for extended-real convex functions · Rockafellar's theorem

TheoremThe Benamou–Brenier formula #

For 1 ≤ p < ∞ and probability measures μ₀, μ₁ on a finite-dimensional real normed space at finite Wasserstein distance, W_p (μ₀, μ₁) ^ p is the least p-action ∫₀¹ ∫ ‖vₜ‖ ^ p dνₜ dt of a curve t ↦ νₜ of finite measures, narrowly continuous on [0, 1] and joining μ₀ to μ₁, solving the continuity equation with velocity v on (0, 1). The minimum is attained by the displacement interpolation of an optimal coupling.

TauCeti.isLeast_lintegral_isContinuityEquation.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E]
  {μ₀ μ₁ : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure μ₀]
  [MeasureTheory.IsProbabilityMeasure μ₁] {p : ENNReal} (hp : 1 ≤ p) (hp_top : p ≠ ⊤)
  (hfin : TauCeti.wassersteinEDist p μ₀ μ₁ ≠ ⊤) :
  IsLeast
    {A |
      ∃ ν v,
        TauCeti.IsContinuityEquation (fun t => ↑(ν t)) v 0 1 ∧
          ContinuousOn ν (Set.Icc 0 1) ∧
            ↑(ν 0) = μ₀ ∧
              ↑(ν 1) = μ₁ ∧ ∫⁻ (t : ℝ) in Set.Ioo 0 1, ∫⁻ (x : E), ‖v t x‖ₑ ^ p.toReal ∂↑(ν t) = A}
    (TauCeti.wassersteinEDist p μ₀ μ₁ ^ p.toReal)

Lean

Formalized in Tau Ceti as TauCeti.isLeast_lintegral_isContinuityEquation.

Other forms

The Benamou–Brenier formula, as an infimum. Formalized in Tau Ceti as TauCeti.wassersteinEDist_rpow_eq_sInf_lintegral_isContinuityEquation.

TauCeti.wassersteinEDist_rpow_eq_sInf_lintegral_isContinuityEquation.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E]
  [BorelSpace E] {μ₀ μ₁ : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure μ₀]
  [MeasureTheory.IsProbabilityMeasure μ₁] {p : ENNReal} (hp : 1 ≤ p) (hp_top : p ≠ ⊤) :
  TauCeti.wassersteinEDist p μ₀ μ₁ ^ p.toReal =
    sInf
      {A |
        ∃ ν v,
          TauCeti.IsContinuityEquation (fun t => ↑(ν t)) v 0 1 ∧
            ContinuousOn ν (Set.Icc 0 1) ∧
              ↑(ν 0) = μ₀ ∧
                ↑(ν 1) = μ₁ ∧
                  ∫⁻ (t : ℝ) in Set.Ioo 0 1, ∫⁻ (x : E), ‖v t x‖ₑ ^ p.toReal ∂↑(ν t) = A}

Sources

LeanTauCeti.isLeast_lintegral_isContinuityEquation · TauCeti.wassersteinEDist_rpow_eq_sInf_lintegral_isContinuityEquation

Uses 2

Proof usesThe Benamou–Brenier lower bound · The Benamou–Brenier upper bound

TheoremLisini's superposition principle in a complete separable metric space #

Let 1 < p < ∞ and let μ be a curve in P_p(X), absolutely continuous on [a, b] with finite p-action, where a < b. There is a probability measure η on C([a, b], X), concentrated on absolutely continuous paths, whose law at each time t ∈ [a, b] is μ t, whose expected p-action is the p-action of μ, and whose averaged speed is the metric speed of μ: |μ'|(t) ^ p = ∫ |γ'|(t) ^ p dη at almost every t ∈ [a, b].

TauCeti.exists_map_IccExtend_eq_lintegral_curveAction_eq.{u_1} {X : Type u_1} [MetricSpace X]
  [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] [CompleteSpace X] {p : ENNReal}
  [Fact (1 ≤ p)] (hp1 : 1 < p) (hp : p ≠ ⊤) {μ : ℝ → TauCeti.WassersteinSpace p X} {a b : ℝ}
  (hab : a < b) (hμ : AbsolutelyContinuousOnInterval μ a b)
  (hA : TauCeti.curveAction p.toReal μ a b ≠ ⊤) :
  ∃ η,
    MeasureTheory.IsProbabilityMeasure η ∧
      (∀ᵐ (γ : C(↑(Set.Icc a b), X)) ∂η, AbsolutelyContinuousOnInterval (Set.IccExtend ⋯ ⇑γ) a b) ∧
        (∀ t ∈ Set.Icc a b,
            MeasureTheory.Measure.map (fun γ => Set.IccExtend ⋯ (⇑γ) t) η = ↑↑(μ t)) ∧
          ∫⁻ (γ : C(↑(Set.Icc a b), X)), TauCeti.curveAction p.toReal (Set.IccExtend ⋯ ⇑γ) a b ∂η =
              TauCeti.curveAction p.toReal μ a b ∧
            ∀ᵐ (t : ℝ),
              t ∈ Set.Icc a b →
                TauCeti.metricDerivative μ t ^ p.toReal =
                  ∫⁻ (γ : C(↑(Set.Icc a b), X)),
                    TauCeti.metricDerivative (Set.IccExtend ⋯ ⇑γ) t ^ p.toReal ∂η

Lean

Formalized in Tau Ceti as TauCeti.exists_map_IccExtend_eq_lintegral_curveAction_eq.

Sources

LeanTauCeti.exists_map_IccExtend_eq_lintegral_curveAction_eq

Uses 6 · Used by 1

Proof usesThe Arzelà–Ascoli theorem in C(X, Y) · Fundamental theorem for absolutely continuous curves, integrability · Hölder estimate along a curve · Hölder's inequality for the integral of a product · Hölder–Markov estimate · Minkowski's integral inequality

Used byUniqueness of Wasserstein geodesics

TheoremUniqueness of Wasserstein geodesics #

Let X be a complete separable metric space and 1 < p < ∞. Suppose that every optimal coupling of μ and ν for the cost d ^ p is π, and that π-almost every pair of points of X is joined by at most one geodesic path. Then any two geodesic segments of P_p (X) from μ to ν agree on [0, 1].

TauCeti.WassersteinSpace.eqOn_of_isGeodesicSegment_of_ae_subsingleton.{u_1} {p : ENNReal}
  [Fact (1 ≤ p)] {X : Type u_1} [MetricSpace X] [CompleteSpace X] [SecondCountableTopology X]
  [MeasurableSpace X] [BorelSpace X] (hp1 : 1 < p) (hp : p ≠ ⊤) {μ ν : TauCeti.WassersteinSpace p X}
  {π : MeasureTheory.Measure (X × X)}
  (hπ :
    ∀ (π' : MeasureTheory.Measure (X × X)),
      TauCeti.IsOptimalCoupling (fun z => edist z.1 z.2 ^ p.toReal) π' ↑↑μ ↑↑ν → π' = π)
  (hgeo : ∀ᵐ (z : X × X) ∂π, {c | c ∈ TauCeti.geodesicPaths X ∧ c 0 = z.1 ∧ c 1 = z.2}.Subsingleton)
  {γ γ' : ℝ → TauCeti.WassersteinSpace p X} (h : TauCeti.IsGeodesicSegment γ μ ν)
  (h' : TauCeti.IsGeodesicSegment γ' μ ν) : Set.EqOn γ γ' (Set.Icc 0 1)

Lean

Formalized in Tau Ceti as TauCeti.WassersteinSpace.eqOn_of_isGeodesicSegment_of_ae_subsingleton.

Sources

LeanTauCeti.WassersteinSpace.eqOn_of_isGeodesicSegment_of_ae_subsingleton

Uses 4

Proof usesHölder estimate along a curve · The Jankov–von Neumann uniformization theorem · Lisini's superposition principle in a complete separable metric space · Lusin's universal-measurability theorem

TheoremMcCann's displacement convexity of internal energies #

Let E be a real inner product space of finite dimension n ≥ 1 with an additive Haar measure ρ, and let U : ℝ → ℝ satisfy U 0 = 0 and McCann's condition: s ↦ sⁿ U(s⁻ⁿ) is convex and nonincreasing on (0, ∞). Let f : E → EReal be convex (convex real epigraph, never ⊥), with real representative F, and let μ be a σ-finite measure, absolutely continuous with respect to ρ and carried by the interior of the effective domain of f. Then the internal energy is convex along the interpolation μₜ = (Tₜ)₊ μ, Tₜ x = (1 - t) • x + t • ∇F x: 𝓤(μₜ) ≤ (1 - t) 𝓤(μ) + t 𝓤((∇F)₊ μ) for t ∈ [0, 1], provided neither endpoint has energy ⊥. The endpoint (∇F)₊ μ need not be absolutely continuous; its singular part is charged at the recession constant U'(∞).

TauCeti.internalEnergy_map_smul_add_smul_gradient_le.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  (ρ : MeasureTheory.Measure E) [ρ.IsAddHaarMeasure] {f : E → EReal} {U : ℝ → ℝ} [Nontrivial E]
  (hU0 : U 0 = 0)
  (hc : ConvexOn ℝ (Set.Ioi 0) fun s => s ^ Module.finrank ℝ E * U (s ^ Module.finrank ℝ E)⁻¹)
  (ha : AntitoneOn (fun s => s ^ Module.finrank ℝ E * U (s ^ Module.finrank ℝ E)⁻¹) (Set.Ioi 0))
  (hf : Convex ℝ {p | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) {μ : MeasureTheory.Measure E}
  [MeasureTheory.SigmaFinite μ] (hμ : μ.AbsolutelyContinuous ρ)
  (hμD : ∀ᵐ (x : E) ∂μ, x ∈ interior {x | f x ≠ ⊤}) (h₀ : TauCeti.internalEnergy U ρ μ ≠ ⊥)
  (h₁ :
    TauCeti.internalEnergy U ρ (MeasureTheory.Measure.map (gradient fun x' => (f x').toReal) μ) ≠ ⊥)
  {t : ℝ} (ht : t ∈ Set.Icc 0 1) :
  TauCeti.internalEnergy U ρ
      (MeasureTheory.Measure.map (fun x => (1 - t) • x + t • gradient (fun x' => (f x').toReal) x)
        μ) ≤
    ↑(1 - t) * TauCeti.internalEnergy U ρ μ +
      ↑t *
        TauCeti.internalEnergy U ρ (MeasureTheory.Measure.map (gradient fun x' => (f x').toReal) μ)

Lean

Formalized in Tau Ceti as TauCeti.internalEnergy_map_smul_add_smul_gradient_le.

Sources

LeanTauCeti.internalEnergy_map_smul_add_smul_gradient_le

Uses 5

Proof usesThe Fenchel–Young inequality · Lebesgue decomposition of the Monge–Ampère measure · Minkowski's determinant inequality · Rademacher's theorem for extended-real convex functions · Rademacher's theorem for locally Lipschitz functions

DefinitionTauCeti.convexSection #

The section of u on Ω at x, with slope ℓ and strict height h.

TauCeti.convexSection.{u_1} {E : Type u_1} [AddCommGroup E] [_root_.Module ℝ E] (Ω : Set E)
  (u : E → ℝ) (x : E) (ℓ : E →ₗ[ℝ] ℝ) (h : ℝ) : Set E

Lean

Formalized in Tau Ceti as TauCeti.convexSection.

Sources

LeanTauCeti.convexSection

Used by 1

Used byThe Vitali covering lemma for sections

DefinitionTauCeti.GromovWassersteinSpace #

Finite-size standard Borel measured kernels modulo weak isomorphism, with the full Gromov–Wasserstein metric. The carrier universe is fixed, but is independent of the target.

TauCeti.GromovWassersteinSpace.{u, v} (p : ENNReal) (Z : Type v) [MetricSpace Z] [Fact (1 ≤ p)] :
  Type (max (u + 1) v)

Lean

Formalized in Tau Ceti as TauCeti.GromovWassersteinSpace.

Sources

LeanTauCeti.GromovWassersteinSpace

DefinitionTauCeti.MetricMeasureSpace.MeasureContraction #

The measure-contraction property MCP(K, N) of Ohta and Sturm, in the form of Cavalletti–Mondino: for every point o of the support of the reference measure m and every measurable A with 0 < m(A) < ∞, some dynamic plan η concentrated on geodesics has law m[|A] = m(A)⁻¹ m|_A at time 0 and law δ_o at time 1, and for every time t the law at time t of η weighted by τ_{K,N}^{(1-t)}(d(γ₀, γ₁))^N is at most m(A)⁻¹ m.

Such a plan is automatically optimal, since m[|A] and δ_o have only one coupling.

TauCeti.MetricMeasureSpace.MeasureContraction.{u_1} {X : Type u_1} [MetricSpace X]
  [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X]
  (M : TauCeti.MetricMeasureSpace X) (K N : ℝ) : Prop

Lean

Formalized in Tau Ceti as TauCeti.MetricMeasureSpace.MeasureContraction.

Sources

LeanTauCeti.MetricMeasureSpace.MeasureContraction

Used by 1

Used byThe Bonnet–Myers diameter bound under MCP(K, N)

TheoremThe Benamou–Brenier lower bound #

Let t ↦ νₜ be a curve of finite measures, narrowly continuous on [a, b] with a ≤ b, solving the continuity equation with velocity v on (a, b), whose initial law ν_a is a probability measure (by conservation of mass, so is ν_b). Then for 1 ≤ p < ∞ the p-Wasserstein distance between the endpoint laws is controlled by the p-action of v: W_p (ν_a, ν_b) ^ p ≤ (b - a) ^ (p - 1) * ∫_a^b ∫ ‖vₜ‖ ^ p dνₜ dt.

On [0, 1] the factor is 1, and this is the inequality W_p (ν₀, ν₁) ^ p ≤ ∫₀¹ ∫ ‖vₜ‖ ^ p dνₜ dt of the Benamou–Brenier formula.

TauCeti.IsContinuityEquation.wassersteinEDist_rpow_le.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E]
  {ν : ℝ → MeasureTheory.FiniteMeasure E} {v : ℝ → E → E} {a b : ℝ}
  (h : TauCeti.IsContinuityEquation (fun t => ↑(ν t)) v a b) (hν : ContinuousOn ν (Set.Icc a b))
  (hab : a ≤ b) [MeasureTheory.IsProbabilityMeasure ↑(ν a)] {p : ENNReal} (hp : 1 ≤ p)
  (hp_top : p ≠ ⊤) :
  TauCeti.wassersteinEDist p ↑(ν a) ↑(ν b) ^ p.toReal ≤
    ENNReal.ofReal ((b - a) ^ (p.toReal - 1)) *
      ∫⁻ (t : ℝ) in Set.Ioo a b, ∫⁻ (x : E), ‖v t x‖ₑ ^ p.toReal ∂↑(ν t)

Lean

Formalized in Tau Ceti as TauCeti.IsContinuityEquation.wassersteinEDist_rpow_le.

Sources

LeanTauCeti.IsContinuityEquation.wassersteinEDist_rpow_le

Uses 3 · Used by 1

Proof usesThe fundamental theorem of calculus for a continuous representative · The Hopf–Lax subsolution inequality · The theorem of Rockafellar and Rüschendorf

Used byThe Benamou–Brenier formula

TheoremThe Bonnet–Myers diameter bound under `MCP(K, N)`#

If M satisfies MCP(K, N) with K > 0 and N > 0, any two points of the support of the reference measure are at distance at most π √((N - 1) / K).

TauCeti.MetricMeasureSpace.MeasureContraction.dist_le.{u_1} {X : Type u_1} [MetricSpace X]
  [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X]
  {M : TauCeti.MetricMeasureSpace X} {K N : ℝ} (h : M.MeasureContraction K N) (hK : 0 < K)
  (hN : 0 < N) {x y : X} (hx : x ∈ M.support) (hy : y ∈ M.support) :
  dist x y ≤ Real.pi * √((N - 1) / K)

Lean

Formalized in Tau Ceti as TauCeti.MetricMeasureSpace.MeasureContraction.dist_le.

Other forms

The Bonnet–Myers diameter bound for the coefficients β. Formalized in Tau Ceti as TauCeti.MetricMeasureSpace.DistortedCurvatureDimension.diam_univ_le.

TauCeti.MetricMeasureSpace.DistortedCurvatureDimension.diam_univ_le.{u_1} {X : Type u_1}
  [MetricSpace X] [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X]
  {M : TauCeti.MetricMeasureSpace X} {β : ℝ → ℝ → ℝ → ENNReal} {N D : ℝ}
  (h : M.DistortedCurvatureDimension β N) (hN : 0 < N) (hD : 0 ≤ D)
  (hβ : ∀ (θ : ℝ), D < θ → β N 1 θ = ⊤) : Metric.diam Set.univ ≤ D

The Bonnet–Myers diameter bound under CD(K, N), for K > 0 and N ≥ 1. Formalized in Tau Ceti as TauCeti.MetricMeasureSpace.CurvatureDimension.diam_support_le.

TauCeti.MetricMeasureSpace.CurvatureDimension.diam_support_le.{u_2} {X : Type u_2} [MetricSpace X]
  [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X]
  {M : TauCeti.MetricMeasureSpace X} {K N : ℝ} (h : M.CurvatureDimension K N) (hK : 0 < K)
  (hN : 1 ≤ N) : Metric.diam M.support ≤ Real.pi * √((N - 1) / K)

The Bonnet–Myers diameter bound under MCP(K, N), for K > 0 and N > 0. Formalized in Tau Ceti as TauCeti.MetricMeasureSpace.MeasureContraction.diam_support_le.

TauCeti.MetricMeasureSpace.MeasureContraction.diam_support_le.{u_1} {X : Type u_1} [MetricSpace X]
  [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X]
  {M : TauCeti.MetricMeasureSpace X} {K N : ℝ} (h : M.MeasureContraction K N) (hK : 0 < K)
  (hN : 0 < N) : Metric.diam M.support ≤ Real.pi * √((N - 1) / K)

Sources

LeanTauCeti.MetricMeasureSpace.MeasureContraction.dist_le · TauCeti.MetricMeasureSpace.DistortedCurvatureDimension.diam_univ_le · TauCeti.MetricMeasureSpace.CurvatureDimension.diam_support_le · TauCeti.MetricMeasureSpace.MeasureContraction.diam_support_le

Uses 2

Statement usesTauCeti.MetricMeasureSpace.MeasureContraction

Proof usesThe generalised Bonnet–Myers theorem under CD(K, N)

TheoremThe Knott–Smith optimality criterion #

On a separable real inner product space, a coupling π of finite measures μ and ν with finite second moments is an optimal plan for the cost ‖x - y‖ ^ 2 / 2 exactly when there is a proper (never ⊥, and finite somewhere) convex, lower semicontinuous u : E → EReal such that y ∈ ∂u(x) for π-almost every (x, y).

TauCeti.IsCoupling.isOptimalCoupling_iff_exists_ae_mem_subdifferential.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [OpensMeasurableSpace (E × E)]
  {μ ν : MeasureTheory.Measure E} {π : MeasureTheory.Measure (E × E)} [OpensMeasurableSpace E]
  [SecondCountableTopology E] [MeasureTheory.IsFiniteMeasure μ] (hπ : TauCeti.IsCoupling π μ ν)
  (hμ : MeasureTheory.MemLp id 2 μ) (hν : MeasureTheory.MemLp id 2 ν) :
  TauCeti.IsOptimalCoupling (fun z => ENNReal.ofReal (‖z.1 - z.2‖ ^ 2 / 2)) π μ ν ↔
    ∃ u,
      Convex ℝ {p | u p.1 ≤ ↑p.2} ∧
        LowerSemicontinuous u ∧
          (∀ (x : E), u x ≠ ⊥) ∧
            (∃ x, u x ≠ ⊤) ∧ ∀ᵐ (z : E × E) ∂π, z.2 ∈ TauCeti.subdifferential (innerₗ E) u z.1

Lean

Formalized in Tau Ceti as TauCeti.IsCoupling.isOptimalCoupling_iff_exists_ae_mem_subdifferential.

Sources

LeanTauCeti.IsCoupling.isOptimalCoupling_iff_exists_ae_mem_subdifferential

Uses 2

Proof usesThe Fenchel–Young inequality · Rockafellar's theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Optimal transport and Wasserstein geometry

TheoremBrenier's theorem#

Lean

Other forms

Sources

TheoremThe Benamou–Brenier formula#

Lean

Other forms

Sources

TheoremLisini's superposition principle in a complete separable metric space#

Lean

Sources

TheoremUniqueness of Wasserstein geodesics#

Lean

Sources

TheoremMcCann's displacement convexity of internal energies#

Lean

Sources

DefinitionTauCeti.convexSection#

Lean

Sources

DefinitionTauCeti.GromovWassersteinSpace#

Lean

Sources

DefinitionTauCeti.MetricMeasureSpace.MeasureContraction#

Lean

Sources

TheoremThe Benamou–Brenier lower bound#

Lean

Sources

TheoremThe Bonnet–Myers diameter bound under MCP(K, N)#

Lean

Other forms

Sources

TheoremThe Knott–Smith optimality criterion#

Lean

Sources

TheoremBrenier's theorem #

TheoremThe Benamou–Brenier formula #

TheoremLisini's superposition principle in a complete separable metric space #

TheoremUniqueness of Wasserstein geodesics #

TheoremMcCann's displacement convexity of internal energies #

DefinitionTauCeti.convexSection #

DefinitionTauCeti.GromovWassersteinSpace #

DefinitionTauCeti.MetricMeasureSpace.MeasureContraction #

TheoremThe Benamou–Brenier lower bound #

TheoremThe Bonnet–Myers diameter bound under `MCP(K, N)`#

TheoremThe Knott–Smith optimality criterion #