Geodesic convexity of energies

Let φ : X → EReal be an energy on a metric space and m : ℝ. The energy is m-convex along a curve γ on [0, 1] if for every t ∈ [0, 1]

φ (γ t) ≤ (1 - t) φ (γ 0) + t φ (γ 1) - (m / 2) t (1 - t) d(γ 0, γ 1)².

It is m-geodesically convex if any two points of its effective domain {x | φ x ≠ ⊤} (which includes points of energy ⊥) are joined by a geodesic segment along which it is m-convex, and m-convex along geodesics if it is m-convex along every geodesic segment joining two points of its effective domain. The parameter m may be negative, and the two notions agree in a uniquely geodesic space. On the Wasserstein space P_p(X) these are the weak and the strong forms of displacement convexity. Geodesic convexity is the basic structural hypothesis of the theory of gradient flows in metric spaces of Ambrosio–Gigli–Savaré; under it the descending slope, which drives curves of maximal slope, takes the global form below.

The convention for m is the one of Mathlib's StrongConvexOn: an m-strongly convex function on a real normed space is m-geodesically convex (StrongConvexOn.geodesicallyConvex). In a CAT(0) space the squared distance from a point is 2-convex along geodesics (TauCeti.convexAlongGeodesics_dist_sq).

The main result identifies the descending slope of a geodesically convex energy with a supremum over all points rather than a limit at x:

|∂φ|(x) = sup_y ((φ x - φ y) / d(x, y) + (m / 2) d(x, y))⁺

at every point x with φ x ≠ ⊤ (TauCeti.GeodesicallyConvex.descendingSlope_eq_iSup). The supremum is written as (φ x - φ y + (m / 2) d(x, y)²)⁺ / d(x, y); its term at y = x is 0. The inequality ≤ holds for every energy (TauCeti.descendingSlope_le_iSup); geodesic convexity gives ≥, by comparing φ with its convexity bound near x along a geodesic towards y. As a supremum of lower semicontinuous functions, the descending slope of a lower semicontinuous geodesically convex energy is lower semicontinuous on its effective domain {x | φ x ≠ ⊤} (TauCeti.GeodesicallyConvex.lowerSemicontinuousOn_descendingSlope), so it is also the relaxed slope there (TauCeti.GeodesicallyConvex.relaxedSlope_eq_descendingSlope).

The three notions are stable under the usual operations, as far as each allows. Convexity along a fixed curve passes to sums (adding the parameters), to nonnegative multiples, to pointwise suprema and to pointwise limits whose endpoint values are ≠ ⊤; it also keeps the effective domain convex along the curve and survives reversing the curve. Convexity along every geodesic inherits all of these, and restricts to every piece of a geodesic. Geodesic convexity, which only provides some geodesic for each pair of points, is stable under positive multiples and under adding an energy that is convex along every geodesic; it need not be stable under sums or suprema of two geodesically convex energies, whose witnessing geodesics may differ. The sums for convexity along every geodesic and for geodesic convexity are taken for energies that never take the value ⊥, so that the effective domain of a sum is the intersection of the effective domains; sums along a fixed curve need no such assumption.

Main definitions

• TauCeti.ConvexAlong m φ γ: φ is m-convex along the curve γ.
• TauCeti.GeodesicallyConvex m φ: any two points with energy ≠ ⊤ are joined by a geodesic segment along which φ is m-convex.
• TauCeti.ConvexAlongGeodesics m φ: φ is m-convex along every geodesic segment joining two points with energy ≠ ⊤.

Main results

• TauCeti.ConvexAlongGeodesics.geodesicallyConvex: in a geodesic space, convexity along every geodesic implies geodesic convexity.
• TauCeti.ConvexAlong.apply_ne_top: the effective domain is convex along a curve of convexity.
• TauCeti.ConvexAlong.apply_add_le_of_forall_le: an m-convex energy grows at least like (m / 2) d(γ 0, γ 1)² away from a minimum at the start of the curve.
• TauCeti.ConvexAlong.add, TauCeti.ConvexAlong.const_mul, TauCeti.ConvexAlong.iSup and TauCeti.ConvexAlong.of_tendsto: convexity along a curve is stable under sums, nonnegative multiples, suprema and pointwise limits; TauCeti.ConvexAlongGeodesics.add, TauCeti.ConvexAlongGeodesics.const_mul, TauCeti.ConvexAlongGeodesics.iSup and TauCeti.ConvexAlongGeodesics.of_tendsto are the versions for convexity along geodesics.
• TauCeti.ConvexAlongGeodesics.convexAlong_comp_lineMap: convexity along geodesics restricts to pieces of geodesics.
• TauCeti.GeodesicallyConvex.add_convexAlongGeodesics and TauCeti.GeodesicallyConvex.const_mul: geodesic convexity is stable under adding an energy convex along geodesics and under positive multiples.
• TauCeti.GeodesicallyConvex.descendingSlope_eq_iSup: the descending slope of an m-geodesically convex energy is its global slope.
• TauCeti.GeodesicallyConvex.lowerSemicontinuousOn_descendingSlope: the descending slope of a lower semicontinuous m-geodesically convex energy is lower semicontinuous on its effective domain.
• TauCeti.GeodesicallyConvex.relaxedSlope_eq_descendingSlope: for such an energy the relaxed and the descending slopes agree on the effective domain.

References

• L. Ambrosio, N. Gigli, G. Savaré, Gradient Flows in Metric Spaces and in the Space of Probability Measures, 2nd ed., Birkhäuser 2008, Chapter 2, Section 2.4, Theorem 2.4.9 and Corollary 2.4.10.

def TauCeti.ConvexAlong {X : Type u_1} [PseudoMetricSpace X] (m : ℝ) (φ : X → EReal) (γ : ℝ → X) : Prop

The energy φ is m-convex along the curve γ, read on [0, 1]: for every t ∈ [0, 1], φ (γ t) ≤ (1 - t) φ (γ 0) + t φ (γ 1) - (m / 2) t (1 - t) d(γ 0, γ 1)².

theorem TauCeti.convexAlong_def {X : Type u_1} [PseudoMetricSpace X] {m : ℝ} {φ : X → EReal} {γ : ℝ → X} : ConvexAlong m φ γ ↔ ∀ t ∈ Set.Icc 0 1, φ (γ t) ≤ ↑(1 - t) * φ (γ 0) + ↑t * φ (γ 1) - ↑(m / 2 * t * (1 - t) * dist (γ 0) (γ 1) ^ 2)

The defining inequality of convexity along a curve.

theorem TauCeti.IsGeodesicSegment.convexAlong_iff {X : Type u_1} [PseudoMetricSpace X] {m : ℝ} {φ : X → EReal} {γ : ℝ → X} {x y : X} (hγ : IsGeodesicSegment γ x y) : ConvexAlong m φ γ ↔ ∀ t ∈ Set.Icc 0 1, φ (γ t) ≤ ↑(1 - t) * φ x + ↑t * φ y - ↑(m / 2 * t * (1 - t) * dist x y ^ 2)

Convexity along a geodesic segment from x to y, in terms of its endpoints.

theorem TauCeti.ConvexAlong.mono {X : Type u_1} [PseudoMetricSpace X] {m m' : ℝ} {φ : X → EReal} {γ : ℝ → X} (h : ConvexAlong m φ γ) (hm : m' ≤ m) : ConvexAlong m' φ γ

Convexity along a curve with a parameter m implies it for every smaller parameter.

def TauCeti.GeodesicallyConvex {X : Type u_1} [PseudoMetricSpace X] (m : ℝ) (φ : X → EReal) : Prop

The energy φ is m-geodesically convex: any two points of its effective domain, that is with φ x ≠ ⊤ (energy ⊥ is allowed), are joined by a geodesic segment along which φ is m-convex.

def TauCeti.ConvexAlongGeodesics {X : Type u_1} [PseudoMetricSpace X] (m : ℝ) (φ : X → EReal) : Prop

The energy φ is m-convex along geodesics: it is m-convex along every geodesic segment joining two points of its effective domain, that is with φ x ≠ ⊤ (energy ⊥ is allowed).

theorem TauCeti.geodesicallyConvex_def {X : Type u_1} [PseudoMetricSpace X] {m : ℝ} {φ : X → EReal} : GeodesicallyConvex m φ ↔ ∀ ⦃x y : X⦄, φ x ≠ ⊤ → φ y ≠ ⊤ → ∃ (γ : ℝ → X), IsGeodesicSegment γ x y ∧ ConvexAlong m φ γ

The defining condition of geodesic convexity.

theorem TauCeti.convexAlongGeodesics_def {X : Type u_1} [PseudoMetricSpace X] {m : ℝ} {φ : X → EReal} : ConvexAlongGeodesics m φ ↔ ∀ ⦃x y : X⦄, φ x ≠ ⊤ → φ y ≠ ⊤ → ∀ ⦃γ : ℝ → X⦄, IsGeodesicSegment γ x y → ConvexAlong m φ γ

The defining condition of convexity along geodesics.

theorem TauCeti.GeodesicallyConvex.mono {X : Type u_1} [PseudoMetricSpace X] {m m' : ℝ} {φ : X → EReal} (h : GeodesicallyConvex m φ) (hm : m' ≤ m) : GeodesicallyConvex m' φ

Geodesic convexity with a parameter m implies it for every smaller parameter.

theorem TauCeti.ConvexAlongGeodesics.mono {X : Type u_1} [PseudoMetricSpace X] {m m' : ℝ} {φ : X → EReal} (h : ConvexAlongGeodesics m φ) (hm : m' ≤ m) : ConvexAlongGeodesics m' φ

Convexity along geodesics with a parameter m implies it for every smaller parameter.

theorem TauCeti.ConvexAlongGeodesics.geodesicallyConvex {X : Type u_1} [PseudoMetricSpace X] {m : ℝ} {φ : X → EReal} [IsGeodesicSpace X] (h : ConvexAlongGeodesics m φ) : GeodesicallyConvex m φ

In a geodesic space, an energy that is m-convex along every geodesic segment is m-geodesically convex.

theorem TauCeti.convexAlongGeodesics_dist_sq {X : Type u_1} [PseudoMetricSpace X] [IsCATZeroSpace X] (z : X) : ConvexAlongGeodesics 2 fun (x : X) => ↑(dist x z ^ 2)

In a CAT(0) space the squared distance from a point is 2-convex along geodesics: this is the CAT(0) comparison inequality d(γ t, z)² ≤ (1 - t) d(x, z)² + t d(y, z)² - t (1 - t) d(x, y)².

Endpoints, restriction and stability

theorem TauCeti.ConvexAlong.apply_ne_top {X : Type u_1} [PseudoMetricSpace X] {m : ℝ} {φ : X → EReal} {γ : ℝ → X} (h : ConvexAlong m φ γ) (h₀ : φ (γ 0) ≠ ⊤) (h₁ : φ (γ 1) ≠ ⊤) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : φ (γ t) ≠ ⊤

The effective domain is convex along a curve of convexity. If φ is m-convex along γ and both endpoint values are ≠ ⊤, then so is φ (γ t) for every t ∈ [0, 1].

theorem TauCeti.ConvexAlong.reverse {X : Type u_1} [PseudoMetricSpace X] {m : ℝ} {φ : X → EReal} {γ : ℝ → X} (h : ConvexAlong m φ γ) : ConvexAlong m φ fun (t : ℝ) => γ (1 - t)

Convexity along a curve is unchanged by running the curve backwards.

theorem TauCeti.ConvexAlong.apply_add_le_of_forall_le {X : Type u_1} [PseudoMetricSpace X] {m : ℝ} {φ : X → EReal} {γ : ℝ → X} (h : ConvexAlong m φ γ) (hmin : ∀ t ∈ Set.Icc 0 1, φ (γ 0) ≤ φ (γ t)) : φ (γ 0) + ↑(m / 2 * dist (γ 0) (γ 1) ^ 2) ≤ φ (γ 1)

Quadratic growth away from a minimum along a curve of convexity. If φ is m-convex along γ and its smallest value along γ on [0, 1] is attained at γ 0, then φ (γ 0) + (m / 2) d(γ 0, γ 1)² ≤ φ (γ 1). Comparing φ (γ 0) with the convexity bound at time t and letting t → 0 gives the inequality; m may be negative.

theorem TauCeti.ConvexAlong.add {X : Type u_1} [PseudoMetricSpace X] {m m' : ℝ} {φ ψ : X → EReal} {γ : ℝ → X} (hφ : ConvexAlong m φ γ) (hψ : ConvexAlong m' ψ γ) : ConvexAlong (m + m') (φ + ψ) γ

Sum of convex energies. If φ is m-convex and ψ is m'-convex along the same curve, then φ + ψ is (m + m')-convex along it.

theorem TauCeti.ConvexAlong.const_mul {X : Type u_1} [PseudoMetricSpace X] {m : ℝ} {φ : X → EReal} {γ : ℝ → X} (h : ConvexAlong m φ γ) {c : ℝ} (hc : 0 ≤ c) : ConvexAlong (c * m) (fun (x : X) => ↑c * φ x) γ

Nonnegative multiple of a convex energy. If φ is m-convex along a curve and c ≥ 0, then c φ is (c m)-convex along it.

theorem TauCeti.ConvexAlong.iSup {X : Type u_1} [PseudoMetricSpace X] {m : ℝ} {γ : ℝ → X} {ι : Sort u_2} {φs : ι → X → EReal} (h : ∀ (i : ι), ConvexAlong m (φs i) γ) : ConvexAlong m (⨆ (i : ι), φs i) γ

Supremum of convex energies. The pointwise supremum of a family of energies, each m-convex along a curve, is m-convex along it.

theorem TauCeti.ConvexAlong.of_tendsto {X : Type u_1} [PseudoMetricSpace X] {m : ℝ} {φ : X → EReal} {γ : ℝ → X} {ι : Type u_2} {l : Filter ι} [l.NeBot] {φs : ι → X → EReal} (h : ∀ᶠ (i : ι) in l, ConvexAlong m (φs i) γ) (hφ : ∀ t ∈ Set.Icc 0 1, Filter.Tendsto (fun (i : ι) => φs i (γ t)) l (nhds (φ (γ t)))) (h₀ : φ (γ 0) ≠ ⊤) (h₁ : φ (γ 1) ≠ ⊤) : ConvexAlong m φ γ

Convexity along a curve passes to pointwise limits. If the energies φs i are eventually m-convex along γ and converge to φ at every point γ t, t ∈ [0, 1], and the endpoint values of φ are ≠ ⊤, then φ is m-convex along γ.

theorem TauCeti.ConvexAlongGeodesics.convexAlong_comp_lineMap {X : Type u_1} [PseudoMetricSpace X] {m : ℝ} {φ : X → EReal} {γ : ℝ → X} {x y : X} (h : ConvexAlongGeodesics m φ) (hγ : IsGeodesicSegment γ x y) (hx : φ x ≠ ⊤) (hy : φ y ≠ ⊤) {a b : ℝ} (ha : a ∈ Set.Icc 0 1) (hb : b ∈ Set.Icc 0 1) : ConvexAlong m φ fun (t : ℝ) => γ ((AffineMap.lineMap a b) t)

Restriction to a piece of a geodesic. If φ is m-convex along geodesics, then along a geodesic segment γ between two points of its effective domain, φ is also m-convex along the piece of γ between any two times a, b ∈ [0, 1], reparametrised over [0, 1].

theorem TauCeti.ConvexAlongGeodesics.add {X : Type u_1} [PseudoMetricSpace X] {m m' : ℝ} {φ ψ : X → EReal} (hφ : ConvexAlongGeodesics m φ) (hψ : ConvexAlongGeodesics m' ψ) (hφ' : ∀ (x : X), φ x ≠ ⊥) (hψ' : ∀ (x : X), ψ x ≠ ⊥) : ConvexAlongGeodesics (m + m') (φ + ψ)

Sum of energies convex along geodesics. If φ is m-convex and ψ is m'-convex along geodesics, and neither takes the value ⊥, then φ + ψ is (m + m')-convex along geodesics.

theorem TauCeti.GeodesicallyConvex.add_convexAlongGeodesics {X : Type u_1} [PseudoMetricSpace X] {m m' : ℝ} {φ ψ : X → EReal} (hφ : GeodesicallyConvex m φ) (hψ : ConvexAlongGeodesics m' ψ) (hφ' : ∀ (x : X), φ x ≠ ⊥) (hψ' : ∀ (x : X), ψ x ≠ ⊥) : GeodesicallyConvex (m + m') (φ + ψ)

Adding an energy convex along geodesics. If φ is m-geodesically convex and ψ is m'-convex along geodesics, and neither takes the value ⊥, then φ + ψ is (m + m')-geodesically convex, along the geodesics that witness the convexity of φ.

theorem TauCeti.GeodesicallyConvex.const_mul {X : Type u_1} [PseudoMetricSpace X] {m : ℝ} {φ : X → EReal} (h : GeodesicallyConvex m φ) {c : ℝ} (hc : 0 < c) : GeodesicallyConvex (c * m) fun (x : X) => ↑c * φ x

Positive multiple of a geodesically convex energy. If φ is m-geodesically convex and c > 0, then c φ is (c m)-geodesically convex.

theorem TauCeti.ConvexAlongGeodesics.const_mul {X : Type u_1} [PseudoMetricSpace X] {m : ℝ} {φ : X → EReal} (h : ConvexAlongGeodesics m φ) {c : ℝ} (hc : 0 ≤ c) : ConvexAlongGeodesics (c * m) fun (x : X) => ↑c * φ x

Nonnegative multiple of an energy convex along geodesics. If φ is m-convex along geodesics and c ≥ 0, then c φ is (c m)-convex along geodesics. For c = 0 this is the zero energy, which is convex along every curve.

theorem TauCeti.ConvexAlongGeodesics.iSup {X : Type u_1} [PseudoMetricSpace X] {m : ℝ} {ι : Sort u_2} {φs : ι → X → EReal} (h : ∀ (i : ι), ConvexAlongGeodesics m (φs i)) : ConvexAlongGeodesics m (⨆ (i : ι), φs i)

Supremum of energies convex along geodesics. The pointwise supremum of a family of energies, each m-convex along geodesics, is m-convex along geodesics.

theorem TauCeti.ConvexAlongGeodesics.of_tendsto {X : Type u_1} [PseudoMetricSpace X] {m : ℝ} {φ : X → EReal} {ι : Type u_2} {l : Filter ι} [l.NeBot] {φs : ι → X → EReal} (h : ∀ᶠ (i : ι) in l, ConvexAlongGeodesics m (φs i)) (hφ : ∀ (x : X), Filter.Tendsto (fun (i : ι) => φs i x) l (nhds (φ x))) : ConvexAlongGeodesics m φ

Convexity along geodesics passes to pointwise limits. If the energies φs i are eventually m-convex along geodesics and converge pointwise to φ, then φ is m-convex along geodesics.

theorem StrongConvexOn.geodesicallyConvex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℝ} {f : E → ℝ} (hf : StrongConvexOn Set.univ m f) : TauCeti.GeodesicallyConvex m fun (x : E) => ↑(f x)

An m-strongly convex function on a real normed space is m-geodesically convex: it is m-convex along the affine segments.

theorem TauCeti.GeodesicallyConvex.le_descendingSlope {X : Type u_1} [MetricSpace X] {m : ℝ} {φ : X → EReal} {x : X} (hφ : GeodesicallyConvex m φ) (hx : φ x ≠ ⊤) (y : X) : (φ x - φ y + ↑(m / 2 * dist x y ^ 2)).toENNReal / edist x y ≤ descendingSlope φ x

Lower bound for the slope of a geodesically convex energy. At a point x with φ x ≠ ⊤ of an m-geodesically convex energy, each term (φ x - φ y + (m / 2) d(x, y)²)⁺ / d(x, y) of the global slope is at most the descending slope.

theorem TauCeti.GeodesicallyConvex.descendingSlope_eq_iSup {X : Type u_1} [MetricSpace X] {m : ℝ} {φ : X → EReal} {x : X} (hφ : GeodesicallyConvex m φ) (hx : φ x ≠ ⊤) : descendingSlope φ x = ⨆ (y : X), (φ x - φ y + ↑(m / 2 * dist x y ^ 2)).toENNReal / edist x y

The slope of a geodesically convex energy is its global slope. If φ is m-geodesically convex and φ x ≠ ⊤, then |∂φ|(x) = sup_y (φ x - φ y + (m / 2) d(x, y)²)⁺ / d(x, y), that is, |∂φ|(x) = sup_{y ≠ x} ((φ x - φ y) / d(x, y) + (m / 2) d(x, y))⁺.

theorem TauCeti.GeodesicallyConvex.lowerSemicontinuousOn_descendingSlope {X : Type u_1} [MetricSpace X] {m : ℝ} {φ : X → EReal} (hφ : GeodesicallyConvex m φ) (hlsc : LowerSemicontinuousOn φ {x : X | φ x ≠ ⊤}) : LowerSemicontinuousOn (descendingSlope φ) {x : X | φ x ≠ ⊤}

The slope of a lower semicontinuous geodesically convex energy is lower semicontinuous on its effective domain {x | φ x ≠ ⊤}, being a supremum of lower semicontinuous functions there.

theorem TauCeti.GeodesicallyConvex.relaxedSlope_eq_descendingSlope {X : Type u_1} [MetricSpace X] {m : ℝ} {φ : X → EReal} {x : X} (hφ : GeodesicallyConvex m φ) (hlsc : LowerSemicontinuousOn φ {x : X | φ x ≠ ⊤}) (hx : φ x ≠ ⊤) : relaxedSlope φ x = descendingSlope φ x

The relaxed slope of a lower semicontinuous geodesically convex energy is its descending slope at every point of its effective domain {x | φ x ≠ ⊤}.