Curves of maximal slope

Let φ : X → EReal be an energy on a metric space with an upper gradient g : X → [0, ∞], and let p, q be conjugate exponents. Along every absolutely continuous curve u, the energy can drop by at most the dissipation

(1/p) ∫_s^t |u'|(r) ^ p dr + (1/q) ∫_s^t g (u r) ^ q dr,

since g controls the rate of change of φ ∘ u by g (u r) |u'|(r), and Young's inequality bounds this product by the integrand above. A p-curve of maximal slope is a curve along which the energy is finite and which, for all times s ≤ t, is absolutely continuous on [s, t] and drops in energy by at least the dissipation: the energy-dissipation inequality

φ (u t) + (1/p) ∫_s^t |u'| ^ p + (1/q) ∫_s^t g (u r) ^ q ≤ φ (u s)

holds. These curves are the metric replacement for the solutions of the gradient flow u' = -∇φ(u) of a smooth energy on a Hilbert space, which are curves of maximal slope for the descending slope (TauCeti.isCurveOfMaximalSlope_of_hasGradientAt).

When g is a strong upper gradient the two bounds meet. Along a curve of maximal slope the energy identity holds: the energy drops by exactly the dissipation. When moreover g ∘ u is almost everywhere measurable, the metric speed and the upper gradient are related by |u'| ^ p = g (u) ^ q almost everywhere, and the energy drop is the p-action. Conversely, a curve absolutely continuous on a compact interval satisfying the energy-dissipation inequality between its endpoints, with the energy finite there, is a curve of maximal slope on the whole interval.

Main definitions

• TauCeti.dissipation p q g u s t: the dissipation (1/p) A_p + (1/q) ∫ g (u r) ^ q of the curve u between s and t, where A_p = TauCeti.curveAction p u s t.
• TauCeti.IsCurveOfMaximalSlope p q φ g u I: u is a p-curve of maximal slope for φ with respect to g on the set of times I.

Main results

• TauCeti.IsStrongUpperGradient.le_add_dissipation: along every absolutely continuous curve the energy drops by at most the dissipation.
• TauCeti.IsCurveOfMaximalSlope.apply_eq_add_dissipation: the energy identity φ (u s) = φ (u t) + dissipation p q g u s t for s ≤ t.
• TauCeti.IsCurveOfMaximalSlope.ae_metricDerivative_rpow_eq: if g ∘ u is a.e.-measurable, |u'| ^ p = g (u) ^ q almost everywhere, and TauCeti.IsCurveOfMaximalSlope.apply_eq_add_curveAction: the energy drop is then the p-action.
• TauCeti.isCurveOfMaximalSlope_Icc_iff: for a curve absolutely continuous on [a, b] it suffices to check finiteness of the energy at a and b and the energy-dissipation inequality between a and b.
• TauCeti.isCurveOfMaximalSlope_of_hasGradientAt: on a Hilbert space, a C¹ solution of u' = -∇f(u) is a 2-curve of maximal slope for the descending slope of f; TauCeti.isCurveOfMaximalSlope_exp_neg_smul is the flow t ↦ e⁻ᵗ x of ‖x‖² / 2.

Implementation notes

Ambrosio–Gigli–Savaré define a curve of maximal slope on an open interval as a locally absolutely continuous curve such that φ ∘ u agrees almost everywhere with a nonincreasing function ψ satisfying ψ' ≤ -(1/p) |u'| ^ p - (1/q) g (u) ^ q almost everywhere. Here the integrated energy-dissipation inequality is required of φ ∘ u itself, on every pair of times of an arbitrary set I (so I may be closed, open or unbounded), together with absolute continuity of u between them. Since φ takes values in EReal, where this inequality holds trivially once φ (u s) = ⊤ or φ (u t) = ⊥, the energy φ ∘ u is moreover required to be finite on I, as the real-valued ψ of Ambrosio–Gigli–Savaré is. Ruling out a modification of φ ∘ u on a null set is a genuine restriction only for weak upper gradients: for a strong upper gradient, Ambrosio–Gigli–Savaré show that φ ∘ u is locally absolutely continuous along their curves of maximal slope.

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 1, Section 1.3.

theorem Real.HolderConjugate.div_add_div_ennreal {p q : ℝ} (hpq : p.HolderConjugate q) (a : ENNReal) : a / ENNReal.ofReal p + a / ENNReal.ofReal q = a

For conjugate exponents p, q, splitting a ∈ [0, ∞] as a / p + a / q recovers a.

noncomputable def TauCeti.dissipation {X : Type u_1} [PseudoEMetricSpace X] (p q : ℝ) (g : X → ENNReal) (u : ℝ → X) (s t : ℝ) : ENNReal

The dissipation of a curve u between s and t for exponents p, q and an upper gradient g: (1/p) ∫ |u'|(r) ^ p dr + (1/q) ∫ g (u r) ^ q dr over the interval between s and t, with the first term the p-action TauCeti.curveAction p u s t.

theorem TauCeti.dissipation_def {X : Type u_1} [PseudoEMetricSpace X] (p q : ℝ) (g : X → ENNReal) (u : ℝ → X) (s t : ℝ) : dissipation p q g u s t = curveAction p u s t / ENNReal.ofReal p + (∫⁻ (r : ℝ) in Set.uIoc s t, g (u r) ^ q) / ENNReal.ofReal q

The defining formula of the dissipation.

theorem TauCeti.dissipation_comm {X : Type u_1} [PseudoEMetricSpace X] (p q : ℝ) (g : X → ENNReal) (u : ℝ → X) (s t : ℝ) : dissipation p q g u s t = dissipation p q g u t s

The dissipation does not depend on the orientation of the interval.

@[simp]

theorem TauCeti.dissipation_self {X : Type u_1} [PseudoEMetricSpace X] (p q : ℝ) (g : X → ENNReal) (u : ℝ → X) (s : ℝ) : dissipation p q g u s s = 0

The dissipation over a degenerate interval vanishes.

theorem TauCeti.dissipation_add {X : Type u_1} [PseudoEMetricSpace X] (p q : ℝ) (g : X → ENNReal) (u : ℝ → X) {a b c : ℝ} (hb : b ∈ Set.uIcc a c) : dissipation p q g u a b + dissipation p q g u b c = dissipation p q g u a c

The dissipation is additive over adjacent intervals.

theorem AbsolutelyContinuousOnInterval.dissipation_eq_lintegral {X : Type u_1} [PseudoMetricSpace X] {p q : ℝ} {g : X → ENNReal} {u : ℝ → X} {s t : ℝ} (hpq : p.HolderConjugate q) (hu : AbsolutelyContinuousOnInterval u s t) : TauCeti.dissipation p q g u s t = ∫⁻ (r : ℝ) in Set.uIoc s t, TauCeti.metricDerivative u r ^ p / ENNReal.ofReal p + g (u r) ^ q / ENNReal.ofReal q

Along a curve absolutely continuous on [s, t], the dissipation is the integral of |u'| ^ p / p + g (u) ^ q / q.

theorem AbsolutelyContinuousOnInterval.lintegral_mul_metricDerivative_le_dissipation {X : Type u_1} [PseudoMetricSpace X] {p q : ℝ} {g : X → ENNReal} {u : ℝ → X} {s t : ℝ} (hpq : p.HolderConjugate q) (hu : AbsolutelyContinuousOnInterval u s t) : ∫⁻ (r : ℝ) in Set.uIoc s t, g (u r) * TauCeti.metricDerivative u r ≤ TauCeti.dissipation p q g u s t

Young's inequality along a curve: the integral of g (u r) |u'|(r) is at most the dissipation.

theorem TauCeti.IsStrongUpperGradient.le_add_dissipation {X : Type u_1} [PseudoMetricSpace X] {p q : ℝ} {φ : X → EReal} {g : X → ENNReal} {u : ℝ → X} {s t : ℝ} (hg : IsStrongUpperGradient φ g) (hpq : p.HolderConjugate q) (hu : AbsolutelyContinuousOnInterval u s t) : φ (u s) ≤ φ (u t) + ↑(dissipation p q g u s t)

Along an absolutely continuous curve, an energy with strong upper gradient g drops by at most the dissipation: φ (u s) ≤ φ (u t) + dissipation p q g u s t.

def TauCeti.IsCurveOfMaximalSlope {X : Type u_1} [PseudoMetricSpace X] (p q : ℝ) (φ : X → EReal) (g : X → ENNReal) (u : ℝ → X) (I : Set ℝ) : Prop

u is a p-curve of maximal slope for the energy φ with respect to the upper gradient g on the set of times I if the energy φ (u s) is finite for every s ∈ I, and for all s ≤ t in I the curve is absolutely continuous on [s, t] and satisfies the energy-dissipation inequality φ (u t) + (1/p) ∫_s^t |u'| ^ p + (1/q) ∫_s^t g (u r) ^ q ≤ φ (u s). Here q is meant to be the conjugate exponent of p.

theorem TauCeti.isCurveOfMaximalSlope_iff {X : Type u_1} [PseudoMetricSpace X] {p q : ℝ} {φ : X → EReal} {g : X → ENNReal} {u : ℝ → X} {I : Set ℝ} : IsCurveOfMaximalSlope p q φ g u I ↔ (∀ ⦃s : ℝ⦄, s ∈ I → φ (u s) ≠ ⊤ ∧ φ (u s) ≠ ⊥) ∧ ∀ ⦃s : ℝ⦄, s ∈ I → ∀ ⦃t : ℝ⦄, t ∈ I → s ≤ t → AbsolutelyContinuousOnInterval u s t ∧ φ (u t) + ↑(dissipation p q g u s t) ≤ φ (u s)

The defining property of a curve of maximal slope.

theorem TauCeti.IsCurveOfMaximalSlope.apply_ne_top {X : Type u_1} [PseudoMetricSpace X] {p q : ℝ} {φ : X → EReal} {g : X → ENNReal} {u : ℝ → X} {I : Set ℝ} {s : ℝ} (h : IsCurveOfMaximalSlope p q φ g u I) (hs : s ∈ I) : φ (u s) ≠ ⊤

The energy is not ⊤ along a curve of maximal slope.

theorem TauCeti.IsCurveOfMaximalSlope.apply_ne_bot {X : Type u_1} [PseudoMetricSpace X] {p q : ℝ} {φ : X → EReal} {g : X → ENNReal} {u : ℝ → X} {I : Set ℝ} {s : ℝ} (h : IsCurveOfMaximalSlope p q φ g u I) (hs : s ∈ I) : φ (u s) ≠ ⊥

The energy is not ⊥ along a curve of maximal slope.

theorem TauCeti.IsCurveOfMaximalSlope.absolutelyContinuousOnInterval {X : Type u_1} [PseudoMetricSpace X] {p q : ℝ} {φ : X → EReal} {g : X → ENNReal} {u : ℝ → X} {I : Set ℝ} {s t : ℝ} (h : IsCurveOfMaximalSlope p q φ g u I) (hs : s ∈ I) (ht : t ∈ I) : AbsolutelyContinuousOnInterval u s t

A curve of maximal slope is absolutely continuous between any two of its times.

theorem TauCeti.IsCurveOfMaximalSlope.apply_add_dissipation_le {X : Type u_1} [PseudoMetricSpace X] {p q : ℝ} {φ : X → EReal} {g : X → ENNReal} {u : ℝ → X} {I : Set ℝ} {s t : ℝ} (h : IsCurveOfMaximalSlope p q φ g u I) (hs : s ∈ I) (ht : t ∈ I) (hst : s ≤ t) : φ (u t) + ↑(dissipation p q g u s t) ≤ φ (u s)

The energy-dissipation inequality along a curve of maximal slope.

theorem TauCeti.IsCurveOfMaximalSlope.mono {X : Type u_1} [PseudoMetricSpace X] {p q : ℝ} {φ : X → EReal} {g : X → ENNReal} {u : ℝ → X} {I J : Set ℝ} (h : IsCurveOfMaximalSlope p q φ g u I) (hJI : J ⊆ I) : IsCurveOfMaximalSlope p q φ g u J

A curve of maximal slope on I is a curve of maximal slope on every subset of I.

theorem TauCeti.IsCurveOfMaximalSlope.antitoneOn {X : Type u_1} [PseudoMetricSpace X] {p q : ℝ} {φ : X → EReal} {g : X → ENNReal} {u : ℝ → X} {I : Set ℝ} (h : IsCurveOfMaximalSlope p q φ g u I) : AntitoneOn (fun (t : ℝ) => φ (u t)) I

The energy is nonincreasing along a curve of maximal slope.

theorem TauCeti.IsCurveOfMaximalSlope.apply_eq_add_dissipation {X : Type u_1} [PseudoMetricSpace X] {p q : ℝ} {φ : X → EReal} {g : X → ENNReal} {u : ℝ → X} {I : Set ℝ} {s t : ℝ} (h : IsCurveOfMaximalSlope p q φ g u I) (hg : IsStrongUpperGradient φ g) (hpq : p.HolderConjugate q) (hs : s ∈ I) (ht : t ∈ I) (hst : s ≤ t) : φ (u s) = φ (u t) + ↑(dissipation p q g u s t)

The energy identity: if g is a strong upper gradient, the energy drops along a curve of maximal slope by exactly the dissipation, φ (u s) = φ (u t) + dissipation p q g u s t.

theorem TauCeti.IsCurveOfMaximalSlope.ae_metricDerivative_rpow_eq {X : Type u_1} [PseudoMetricSpace X] {p q : ℝ} {φ : X → EReal} {g : X → ENNReal} {u : ℝ → X} {I : Set ℝ} {s t : ℝ} (h : IsCurveOfMaximalSlope p q φ g u I) (hg : IsStrongUpperGradient φ g) (hpq : p.HolderConjugate q) (hs : s ∈ I) (ht : t ∈ I) (hgu : AEMeasurable (fun (r : ℝ) => g (u r)) (MeasureTheory.volume.restrict (Set.uIoc s t))) : ∀ᵐ (r : ℝ) ∂MeasureTheory.volume.restrict (Set.uIoc s t), metricDerivative u r ^ p = g (u r) ^ q

Along a curve of maximal slope for a strong upper gradient g, if g ∘ u is a.e.-measurable between s and t, the metric speed and the upper gradient satisfy |u'| ^ p = g (u) ^ q almost everywhere there.

theorem TauCeti.IsCurveOfMaximalSlope.apply_eq_add_curveAction {X : Type u_1} [PseudoMetricSpace X] {p q : ℝ} {φ : X → EReal} {g : X → ENNReal} {u : ℝ → X} {I : Set ℝ} {s t : ℝ} (h : IsCurveOfMaximalSlope p q φ g u I) (hg : IsStrongUpperGradient φ g) (hpq : p.HolderConjugate q) (hs : s ∈ I) (ht : t ∈ I) (hst : s ≤ t) (hgu : AEMeasurable (fun (r : ℝ) => g (u r)) (MeasureTheory.volume.restrict (Set.uIoc s t))) : φ (u s) = φ (u t) + ↑(curveAction p u s t)

The energy identity in terms of the action: along a curve of maximal slope for a strong upper gradient g, if g ∘ u is a.e.-measurable between s and t, the energy drops by exactly the p-action, φ (u s) = φ (u t) + A_p(u).

theorem TauCeti.IsCurveOfMaximalSlope.apply_eq_add_lintegral_rpow {X : Type u_1} [PseudoMetricSpace X] {p q : ℝ} {φ : X → EReal} {g : X → ENNReal} {u : ℝ → X} {I : Set ℝ} {s t : ℝ} (h : IsCurveOfMaximalSlope p q φ g u I) (hg : IsStrongUpperGradient φ g) (hpq : p.HolderConjugate q) (hs : s ∈ I) (ht : t ∈ I) (hst : s ≤ t) (hgu : AEMeasurable (fun (r : ℝ) => g (u r)) (MeasureTheory.volume.restrict (Set.uIoc s t))) : φ (u s) = φ (u t) + ↑(∫⁻ (r : ℝ) in Set.uIoc s t, g (u r) ^ q)

The energy identity in terms of the upper gradient: along a curve of maximal slope for a strong upper gradient g, if g ∘ u is a.e.-measurable between s and t, then φ (u s) = φ (u t) + ∫_s^t g (u r) ^ q dr.

theorem TauCeti.isCurveOfMaximalSlope_Icc_iff {X : Type u_1} [PseudoMetricSpace X] {p q : ℝ} {φ : X → EReal} {g : X → ENNReal} {u : ℝ → X} {a b : ℝ} (hg : IsStrongUpperGradient φ g) (hpq : p.HolderConjugate q) (hab : a ≤ b) (hu : AbsolutelyContinuousOnInterval u a b) : IsCurveOfMaximalSlope p q φ g u (Set.Icc a b) ↔ φ (u a) ≠ ⊤ ∧ φ (u b) ≠ ⊥ ∧ φ (u b) + ↑(dissipation p q g u a b) ≤ φ (u a)

For a strong upper gradient g, a curve absolutely continuous on [a, b] is a curve of maximal slope on [a, b] as soon as φ (u a) < ∞, φ (u b) > -∞ and the energy-dissipation inequality holds between a and b.

theorem TauCeti.isCurveOfMaximalSlope_of_hasGradientAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {u G : ℝ → E} {I : Set ℝ} [I.OrdConnected] (hf : ∀ t ∈ I, HasGradientAt f (G t) (u t)) (hu : ∀ t ∈ I, HasDerivAt u (-G t) t) (hG : ContinuousOn G I) : IsCurveOfMaximalSlope 2 2 (fun (x : E) => ↑(f x)) (descendingSlope fun (x : E) => ↑(f x)) u I

On a Hilbert space, a solution u' = -∇f(u) of the gradient flow of f with continuous velocity is a 2-curve of maximal slope for f with respect to its descending slope: along it the energy drops at rate ‖∇f(u)‖² = (1/2) |u'| ^ 2 + (1/2) |∂f| (u) ^ 2.

theorem TauCeti.isCurveOfMaximalSlope_exp_neg_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (x : E) : IsCurveOfMaximalSlope 2 2 (fun (y : E) => ↑(‖y‖ ^ 2 / 2)) (descendingSlope fun (y : E) => ↑(‖y‖ ^ 2 / 2)) (fun (t : ℝ) => Real.exp (-t) • x) Set.univ

The flow t ↦ e⁻ᵗ x of the energy ‖x‖² / 2 on a Hilbert space is a 2-curve of maximal slope for the descending slope of the energy.