Stability of convexity along generalized geodesics

Convexity witnessed by some generalized-geodesic plan is not in general stable under addition: two energies may choose different plans. TauCeti.ConvexAlongGeneralizedGeodesics requires the convexity inequality along every such plan based at a fixed law. On separable Banach spaces it implies TauCeti.GeneralizedGeodesicallyConvex. The every-plan condition is stable under sums of energies that never take ⊥, nonnegative multiples, suprema and pointwise limits. Adding such an energy to a TauCeti.GeneralizedGeodesicallyConvex energy preserves the latter condition, with the sum of the convexity parameters, provided neither energy takes ⊥. These rules allow composite energies to use the uniqueness theorem for the Jordan–Kinderlehrer–Otto step without assuming a common witnessing plan.

The correction uses the quadratic cost of the endpoint coupling carried by the three-plan, not the squared Wasserstein distance of its endpoints. In a separable Hilbert space the squared distance from the base law satisfies the every-plan condition with parameter 2.

References

• L. Ambrosio, N. Gigli, G. Savaré, Gradient Flows in Metric Spaces and in the Space of Probability Measures, 2nd ed., Birkhäuser 2008, §9.2 and Chapter 4, Assumption 4.0.1.

theorem TauCeti.ConvexAlongGeneralizedGeodesicPlan.apply_ne_top {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] {m : ℝ} {φ : WassersteinSpace 2 E → EReal} {ν₀ ν₁ : WassersteinSpace 2 E} {γ : MeasureTheory.Measure (E × E × E)} (h : ConvexAlongGeneralizedGeodesicPlan m φ ν₀ ν₁ γ) (h₀ : φ ν₀ ≠ ⊤) (h₁ : φ ν₁ ≠ ⊤) {ν : WassersteinSpace 2 E} {t : ℝ} (ht : t ∈ Set.Icc 0 1) (hν : ↑↑ν = generalizedGeodesic γ t) : φ ν ≠ ⊤

Along a fixed three-plan, convexity preserves the effective domain when both endpoint energies are different from ⊤.

theorem TauCeti.ConvexAlongGeneralizedGeodesicPlan.add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] {m m' : ℝ} {φ ψ : WassersteinSpace 2 E → EReal} {ν₀ ν₁ : WassersteinSpace 2 E} {γ : MeasureTheory.Measure (E × E × E)} (hφ : ConvexAlongGeneralizedGeodesicPlan m φ ν₀ ν₁ γ) (hψ : ConvexAlongGeneralizedGeodesicPlan m' ψ ν₀ ν₁ γ) : ConvexAlongGeneralizedGeodesicPlan (m + m') (φ + ψ) ν₀ ν₁ γ

Energies convex along the same three-plan add, with the sum of their parameters.

theorem TauCeti.ConvexAlongGeneralizedGeodesicPlan.const_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] {m : ℝ} {φ : WassersteinSpace 2 E → EReal} {ν₀ ν₁ : WassersteinSpace 2 E} {γ : MeasureTheory.Measure (E × E × E)} (h : ConvexAlongGeneralizedGeodesicPlan m φ ν₀ ν₁ γ) {c : ℝ} (hc : 0 ≤ c) : ConvexAlongGeneralizedGeodesicPlan (c * m) (fun (ν : WassersteinSpace 2 E) => ↑c * φ ν) ν₀ ν₁ γ

Nonnegative multiples preserve convexity along a fixed three-plan, multiplying the parameter by the same scalar.

theorem TauCeti.ConvexAlongGeneralizedGeodesicPlan.iSup {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] {m : ℝ} {ν₀ ν₁ : WassersteinSpace 2 E} {γ : MeasureTheory.Measure (E × E × E)} {ι : Sort u_2} {φs : ι → WassersteinSpace 2 E → EReal} (h : ∀ (i : ι), ConvexAlongGeneralizedGeodesicPlan m (φs i) ν₀ ν₁ γ) : ConvexAlongGeneralizedGeodesicPlan m (⨆ (i : ι), φs i) ν₀ ν₁ γ

The pointwise supremum of energies convex along a fixed three-plan, with a common parameter, is convex along that plan. The index type may be empty.

theorem TauCeti.ConvexAlongGeneralizedGeodesicPlan.of_tendsto {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] {m : ℝ} {φ : WassersteinSpace 2 E → EReal} {ν₀ ν₁ : WassersteinSpace 2 E} {γ : MeasureTheory.Measure (E × E × E)} {ι : Type u_2} {l : Filter ι} [l.NeBot] {φs : ι → WassersteinSpace 2 E → EReal} (h : ∀ᶠ (i : ι) in l, ConvexAlongGeneralizedGeodesicPlan m (φs i) ν₀ ν₁ γ) (hφ : ∀ (ν : WassersteinSpace 2 E), Filter.Tendsto (fun (i : ι) => φs i ν) l (nhds (φ ν))) (h₀ : φ ν₀ ≠ ⊤) (h₁ : φ ν₁ ≠ ⊤) : ConvexAlongGeneralizedGeodesicPlan m φ ν₀ ν₁ γ

Convexity along a fixed three-plan passes to pointwise limits whose endpoint energies are different from ⊤.

def TauCeti.ConvexAlongGeneralizedGeodesics {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] (m : ℝ) (φ : WassersteinSpace 2 E → EReal) (μ : WassersteinSpace 2 E) : Prop

The energy φ is m-convex along every quadratic generalized-geodesic plan based at μ whose endpoints have energy different from ⊤. The remainder uses the quadratic cost of the endpoint coupling carried by the plan; endpoint energy ⊥ is allowed.

theorem TauCeti.convexAlongGeneralizedGeodesics_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] {m : ℝ} {φ : WassersteinSpace 2 E → EReal} {μ : WassersteinSpace 2 E} : ConvexAlongGeneralizedGeodesics m φ μ ↔ ∀ ⦃ν₀ ν₁ : WassersteinSpace 2 E⦄, φ ν₀ ≠ ⊤ → φ ν₁ ≠ ⊤ → ∀ ⦃γ : MeasureTheory.Measure (E × E × E)⦄, IsGeneralizedGeodesicPlan 2 γ ↑↑μ ↑↑ν₀ ↑↑ν₁ → ConvexAlongGeneralizedGeodesicPlan m φ ν₀ ν₁ γ

The defining condition for convexity along every generalized-geodesic plan.

theorem TauCeti.ConvexAlongGeneralizedGeodesics.apply_ne_top {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] {m : ℝ} {φ : WassersteinSpace 2 E → EReal} {μ : WassersteinSpace 2 E} (h : ConvexAlongGeneralizedGeodesics m φ μ) {ν₀ ν₁ ν : WassersteinSpace 2 E} (h₀ : φ ν₀ ≠ ⊤) (h₁ : φ ν₁ ≠ ⊤) {γ : MeasureTheory.Measure (E × E × E)} (hγ : IsGeneralizedGeodesicPlan 2 γ ↑↑μ ↑↑ν₀ ↑↑ν₁) {t : ℝ} (ht : t ∈ Set.Icc 0 1) (hν : ↑↑ν = generalizedGeodesic γ t) : φ ν ≠ ⊤

The effective domain is preserved along every generalized-geodesic plan.

theorem TauCeti.ConvexAlongGeneralizedGeodesics.mono {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] {m m' : ℝ} {φ : WassersteinSpace 2 E → EReal} {μ : WassersteinSpace 2 E} (h : ConvexAlongGeneralizedGeodesics m φ μ) (hm : m' ≤ m) : ConvexAlongGeneralizedGeodesics m' φ μ

Convexity along every generalized-geodesic plan persists with a smaller parameter.

theorem TauCeti.ConvexAlongGeneralizedGeodesics.add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] {m m' : ℝ} {φ ψ : WassersteinSpace 2 E → EReal} {μ : WassersteinSpace 2 E} (hφ : ConvexAlongGeneralizedGeodesics m φ μ) (hψ : ConvexAlongGeneralizedGeodesics m' ψ μ) (hφ' : ∀ (ν : WassersteinSpace 2 E), φ ν ≠ ⊥) (hψ' : ∀ (ν : WassersteinSpace 2 E), ψ ν ≠ ⊥) : ConvexAlongGeneralizedGeodesics (m + m') (φ + ψ) μ

Sums of energies convex along every generalized-geodesic plan have the sum parameter. Excluding ⊥ ensures that finite energy of the sum implies finite energy of both summands.

theorem TauCeti.GeneralizedGeodesicallyConvex.add_convexAlongGeneralizedGeodesics {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] {m m' : ℝ} {φ ψ : WassersteinSpace 2 E → EReal} {μ : WassersteinSpace 2 E} (hφ : GeneralizedGeodesicallyConvex m φ μ) (hψ : ConvexAlongGeneralizedGeodesics m' ψ μ) (hφ' : ∀ (ν : WassersteinSpace 2 E), φ ν ≠ ⊥) (hψ' : ∀ (ν : WassersteinSpace 2 E), ψ ν ≠ ⊥) : GeneralizedGeodesicallyConvex (m + m') (φ + ψ) μ

Adding an energy convex along every generalized-geodesic plan preserves convexity along some plan, using the witnessing plan of the first energy. Neither energy may take ⊥.

theorem TauCeti.ConvexAlongGeneralizedGeodesics.const_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] {m : ℝ} {φ : WassersteinSpace 2 E → EReal} {μ : WassersteinSpace 2 E} (h : ConvexAlongGeneralizedGeodesics m φ μ) {c : ℝ} (hc : 0 ≤ c) : ConvexAlongGeneralizedGeodesics (c * m) (fun (ν : WassersteinSpace 2 E) => ↑c * φ ν) μ

Nonnegative multiples preserve convexity along every generalized-geodesic plan, multiplying the parameter by the same scalar. At scalar zero the energy is identically zero.

theorem TauCeti.GeneralizedGeodesicallyConvex.const_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] {m : ℝ} {φ : WassersteinSpace 2 E → EReal} {μ : WassersteinSpace 2 E} (h : GeneralizedGeodesicallyConvex m φ μ) {c : ℝ} (hc : 0 < c) : GeneralizedGeodesicallyConvex (c * m) (fun (ν : WassersteinSpace 2 E) => ↑c * φ ν) μ

Positive multiples preserve convexity witnessed by some generalized-geodesic plan.

theorem TauCeti.ConvexAlongGeneralizedGeodesics.iSup {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] {m : ℝ} {μ : WassersteinSpace 2 E} {ι : Sort u_2} {φs : ι → WassersteinSpace 2 E → EReal} (h : ∀ (i : ι), ConvexAlongGeneralizedGeodesics m (φs i) μ) : ConvexAlongGeneralizedGeodesics m (⨆ (i : ι), φs i) μ

The pointwise supremum preserves convexity along every generalized-geodesic plan with a common parameter. This includes the empty supremum, the energy identically ⊥.

theorem TauCeti.ConvexAlongGeneralizedGeodesics.of_tendsto {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] {m : ℝ} {φ : WassersteinSpace 2 E → EReal} {μ : WassersteinSpace 2 E} {ι : Type u_2} {l : Filter ι} [l.NeBot] {φs : ι → WassersteinSpace 2 E → EReal} (h : ∀ᶠ (i : ι) in l, ConvexAlongGeneralizedGeodesics m (φs i) μ) (hφ : ∀ (ν : WassersteinSpace 2 E), Filter.Tendsto (fun (i : ι) => φs i ν) l (nhds (φ ν))) : ConvexAlongGeneralizedGeodesics m φ μ

Convexity along every generalized-geodesic plan passes to pointwise limits. No compactness or convergence of witnessing plans is needed, because the inequality holds along each fixed plan.

theorem TauCeti.ConvexAlongGeneralizedGeodesics.generalizedGeodesicallyConvex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] {m : ℝ} {φ : WassersteinSpace 2 E → EReal} {μ : WassersteinSpace 2 E} [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] (h : ConvexAlongGeneralizedGeodesics m φ μ) : GeneralizedGeodesicallyConvex m φ μ

On a separable Banach space, convexity along every generalized-geodesic plan implies convexity witnessed by some plan, since optimal plans out of the base law can be glued.

theorem TauCeti.convexAlongGeneralizedGeodesics_dist_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] (μ : WassersteinSpace 2 E) : ConvexAlongGeneralizedGeodesics 2 (fun (ν : WassersteinSpace 2 E) => ↑(dist μ ν ^ 2)) μ

In a separable Hilbert space, the squared Wasserstein distance from the base law is 2-convex along every generalized-geodesic plan based at that law.