Strong upper gradients

A function g : X → [0, ∞] is a strong upper gradient of an energy φ : X → EReal on a metric space if along every absolutely continuous curve γ the energy varies by at most the integral of g against the metric speed:

|φ (γ b) - φ (γ a)| ≤ ∫_a^b g (γ r) |γ'|(r) dr.

Upper gradients replace the norm of the gradient in the theory of gradient flows in metric spaces of Ambrosio–Gigli–Savaré: curves of maximal slope and the energy-dissipation inequality are stated with respect to an upper gradient, and the descending slope TauCeti.descendingSlope is the canonical candidate.

Main definitions

• TauCeti.IsStrongUpperGradient φ g: g is a strong upper gradient of φ.

Main results

• the chain rule inequality |(f ∘ γ)'(t)| ≤ |∂f|(γ t) |γ'|(t) at every time where f ∘ γ is differentiable and the right-hand side is not of the form 0 · ∞, comparing the derivative of a real function along a curve with its descending slope and the metric derivative of the curve (HasDerivAt.enorm_le_descendingSlope_mul_metricDerivative);
• the descending slope of a locally Lipschitz function is a strong upper gradient (LocallyLipschitz.isStrongUpperGradient_descendingSlope);
• for a real function with strong upper gradient g, the bound |f (γ a) - f (γ b)| ≤ ∫ g (γ r) |γ'|(r) dr (TauCeti.IsStrongUpperGradient.edist_le_lintegral), so that along an absolutely continuous curve on which g (γ r) |γ'|(r) is integrable the function is absolutely continuous (TauCeti.IsStrongUpperGradient.absolutelyContinuousOnInterval_comp).

Implementation notes

Since φ takes values in EReal, the absolute value of a difference is replaced by the two one-sided inequalities φ (γ a) ≤ φ (γ b) + ∫ ... and φ (γ b) ≤ φ (γ a) + ∫ ...; the definition states the first for every absolutely continuous curve on [a, b], and the second follows by exchanging a and b. When the integral is finite this is exactly the two-sided bound, and it forces φ (γ a) = ⊤ exactly when φ (γ b) = ⊤.

The integral is the lower Lebesgue integral lintegral, which is defined for every function. Ambrosio–Gigli–Savaré require g ∘ γ to be Borel so that the integral makes sense; for a Borel g the two definitions agree, since γ is continuous.

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.2.

def TauCeti.IsStrongUpperGradient {X : Type u_1} [PseudoMetricSpace X] (φ : X → EReal) (g : X → ENNReal) : Prop

g is a strong upper gradient of the energy φ if for every curve γ absolutely continuous on [a, b], φ (γ a) ≤ φ (γ b) + ∫⁻ r in Ι a b, g (γ r) * |γ'|(r). Exchanging a and b gives the reverse inequality, so for a finite integral this is the bound |φ (γ b) - φ (γ a)| ≤ ∫ g (γ r) |γ'|(r) dr.

theorem TauCeti.isStrongUpperGradient_iff {X : Type u_1} [PseudoMetricSpace X] {φ : X → EReal} {g : X → ENNReal} : IsStrongUpperGradient φ g ↔ ∀ ⦃γ : ℝ → X⦄ ⦃a b : ℝ⦄, AbsolutelyContinuousOnInterval γ a b → φ (γ a) ≤ φ (γ b) + ↑(∫⁻ (r : ℝ) in Set.uIoc a b, g (γ r) * metricDerivative γ r)

The defining property of a strong upper gradient.

theorem TauCeti.IsStrongUpperGradient.le_add_lintegral {X : Type u_1} [PseudoMetricSpace X] {φ : X → EReal} {g : X → ENNReal} (hg : IsStrongUpperGradient φ g) {γ : ℝ → X} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) : φ (γ a) ≤ φ (γ b) + ↑(∫⁻ (r : ℝ) in Set.uIoc a b, g (γ r) * metricDerivative γ r)

Along a curve γ absolutely continuous on [a, b], an energy with strong upper gradient g satisfies φ (γ a) ≤ φ (γ b) + ∫⁻ r in Ι a b, g (γ r) * |γ'|(r).

theorem TauCeti.IsStrongUpperGradient.mono {X : Type u_1} [PseudoMetricSpace X] {φ : X → EReal} {g g' : X → ENNReal} (hg : IsStrongUpperGradient φ g) (hgg' : ∀ (x : X), g x ≤ g' x) : IsStrongUpperGradient φ g'

A function above a strong upper gradient is a strong upper gradient.

theorem TauCeti.IsStrongUpperGradient.edist_le_lintegral {X : Type u_1} [PseudoMetricSpace X] {g : X → ENNReal} {f : X → ℝ} (hg : IsStrongUpperGradient (fun (x : X) => ↑(f x)) g) {γ : ℝ → X} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) : edist (f (γ a)) (f (γ b)) ≤ ∫⁻ (r : ℝ) in Set.uIoc a b, g (γ r) * metricDerivative γ r

For a real function f with strong upper gradient g and a curve γ absolutely continuous on [a, b], |f (γ a) - f (γ b)| ≤ ∫⁻ r in Ι a b, g (γ r) * |γ'|(r).

theorem TauCeti.IsStrongUpperGradient.absolutelyContinuousOnInterval_comp {X : Type u_1} [PseudoMetricSpace X] {g : X → ENNReal} {f : X → ℝ} (hg : IsStrongUpperGradient (fun (x : X) => ↑(f x)) g) {γ : ℝ → X} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hfin : ∫⁻ (r : ℝ) in Set.uIoc a b, g (γ r) * metricDerivative γ r ≠ ⊤) : AbsolutelyContinuousOnInterval (fun (r : ℝ) => f (γ r)) a b

Along an absolutely continuous curve γ on [a, b] with ∫⁻ r in Ι a b, g (γ r) * |γ'|(r) < ∞, a real function with strong upper gradient g is absolutely continuous on [a, b].

theorem HasDerivAt.enorm_le_descendingSlope_mul_metricDerivative {X : Type u_1} [EMetricSpace X] {f : X → ℝ} {γ : ℝ → X} {t D : ℝ} (hD : HasDerivAt (fun (r : ℝ) => f (γ r)) D t) (h₀ : TauCeti.descendingSlope (fun (x : X) => ↑(f x)) (γ t) ≠ 0 ∨ TauCeti.metricDerivative γ t ≠ ⊤) (htop : TauCeti.descendingSlope (fun (x : X) => ↑(f x)) (γ t) ≠ ⊤ ∨ TauCeti.metricDerivative γ t ≠ 0) : ‖D‖ₑ ≤ TauCeti.descendingSlope (fun (x : X) => ↑(f x)) (γ t) * TauCeti.metricDerivative γ t

Chain rule inequality for the descending slope: if f ∘ γ has derivative D at t, then |D| ≤ |∂f|(γ t) * |γ'|(t). The hypotheses h₀ and htop exclude the products 0 * ∞ and ∞ * 0, for which the inequality can fail.

theorem LocallyLipschitz.isStrongUpperGradient_descendingSlope {X : Type u_1} [MetricSpace X] {f : X → ℝ} (hf : LocallyLipschitz f) : TauCeti.IsStrongUpperGradient (fun (x : X) => ↑(f x)) (TauCeti.descendingSlope fun (x : X) => ↑(f x))

The descending slope of a locally Lipschitz function is a strong upper gradient: along every absolutely continuous curve γ on [a, b], |f (γ b) - f (γ a)| ≤ ∫ |∂f|(γ r) |γ'|(r) dr.