The descending slope of an energy

For an extended-real energy φ : X → EReal on an extended metric space, the descending slope (or local slope) of φ at x is

|∂φ|(x) = limsup_{y → x, y ≠ x} (φ x - φ y)⁺ / d(x, y),

the steepest rate at which φ can decrease near x. It is the metric replacement for the norm of the gradient: for a function on a real normed space that is differentiable at x, the descending slope is the operator norm of the derivative (HasFDerivAt.descendingSlope_eq). The descending slope is the basic object of the theory of gradient flows in metric spaces of Ambrosio–Gigli–Savaré: curves of maximal slope, the energy-dissipation inequality and the slope estimates for minimizing movements are all phrased through it.

The positive part (φ x - φ y)⁺ is EReal.toENNReal (φ x - φ y). Ambrosio–Gigli–Savaré define the slope only on the effective domain {x | φ x ≠ ⊤}; the formula here is total, and its value off the effective domain carries no meaning.

Main definitions

• TauCeti.descendingSlope φ x: the descending slope of φ at x, an extended nonnegative real.

Main results

• Isometry.descendingSlope_comp: an isometry preserves the slope where its range contains a neighbourhood, in particular when restricting an energy to an open subset.
• TauCeti.descendingSlope_le_of_eventually_le: an upper bound for the slope from a local bound on the decrease of φ.
• TauCeti.le_descendingSlope_of_tendsto: a lower bound for the slope from the rates of decrease of φ along a map tending to x.
• TauCeti.descendingSlope_le_iSup: on a metric space, the slope is at most the global slope sup_y (φ x - φ y + (m / 2) d(x, y)²)⁺ / d(x, y), for every m.
• IsLocalMin.descendingSlope_eq_zero: the slope vanishes at a local minimum.
• LipschitzOnWith.descendingSlope_le and LipschitzWith.descendingSlope_le: the slope of a function that is K-Lipschitz near x is at most K.
• TauCeti.descendingSlope_const_mul: positive homogeneity of the slope of real-valued functions.
• HasFDerivAt.descendingSlope_eq: on a real normed space the slope of a function differentiable at x is the norm of its derivative; HasDerivAt.descendingSlope_eq is the one-variable case.

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.

noncomputable def TauCeti.descendingSlope {X : Type u_1} [EMetricSpace X] (φ : X → EReal) (x : X) : ENNReal

The descending slope (or local slope) of an energy φ at x: the upper limit, as y → x with y ≠ x, of the rate of decrease (φ x - φ y)⁺ / d(x, y). At an isolated point the slope is 0.

theorem TauCeti.descendingSlope_def {X : Type u_1} [EMetricSpace X] (φ : X → EReal) (x : X) : descendingSlope φ x = Filter.limsup (fun (y : X) => (φ x - φ y).toENNReal / edist x y) (nhdsWithin x {x}ᶜ)

The defining formula of the descending slope, as an upper limit of rates of decrease.

theorem Isometry.descendingSlope_comp {X : Type u_1} [EMetricSpace X] {Y : Type u_2} [EMetricSpace Y] {f : X → Y} (hf : Isometry f) (φ : Y → EReal) (x : X) (hx : Set.range f ∈ nhds (f x)) : TauCeti.descendingSlope (φ ∘ f) x = TauCeti.descendingSlope φ (f x)

Pulling an energy back along an isometry preserves its descending slope at a point where the range of the isometry contains a neighbourhood. In particular, restricting an energy to an open subset leaves the descending slope unchanged there.

theorem TauCeti.descendingSlope_coe {X : Type u_1} [EMetricSpace X] (f : X → ℝ) (x : X) : descendingSlope (fun (y : X) => ↑(f y)) x = Filter.limsup (fun (y : X) => ENNReal.ofReal (f x - f y) / edist x y) (nhdsWithin x {x}ᶜ)

For a real-valued function, the positive part in the descending slope is ENNReal.ofReal (f x - f y).

theorem TauCeti.descendingSlope_le_of_eventually_le {X : Type u_1} [EMetricSpace X] {φ : X → EReal} {x : X} {C : ENNReal} (h : ∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, (φ x - φ y).toENNReal ≤ C * edist x y) : descendingSlope φ x ≤ C

If near x the energy decreases at most like C * d(x, y), then the descending slope of φ at x is at most C.

theorem TauCeti.le_descendingSlope_of_tendsto {X : Type u_1} [EMetricSpace X] {φ : X → EReal} {x : X} {α : Type u_2} {l : Filter α} [l.NeBot] {g : α → X} {f : α → ENNReal} {L : ENNReal} (hg : Filter.Tendsto g l (nhdsWithin x {x}ᶜ)) (hf : Filter.Tendsto f l (nhds L)) (hle : ∀ᶠ (t : α) in l, f t ≤ (φ x - φ (g t)).toENNReal / edist x (g t)) : L ≤ descendingSlope φ x

If g tends to x from outside x, and along g the rates of decrease (φ x - φ (g t))⁺ / d(x, g t) are eventually at least f t, where f t tends to L, then the descending slope of φ at x is at least L.

theorem IsLocalMin.descendingSlope_eq_zero {X : Type u_1} [EMetricSpace X] {φ : X → EReal} {x : X} (h : IsLocalMin φ x) : TauCeti.descendingSlope φ x = 0

The descending slope vanishes at a local minimum.

@[simp]

theorem TauCeti.descendingSlope_const {X : Type u_1} [EMetricSpace X] (c : EReal) (x : X) : descendingSlope (fun (x : X) => c) x = 0

The descending slope of a constant energy vanishes.

theorem LipschitzOnWith.descendingSlope_le {X : Type u_1} [EMetricSpace X] {x : X} {f : X → ℝ} {K : NNReal} {s : Set X} (hf : LipschitzOnWith K f s) (hs : s ∈ nhds x) : TauCeti.descendingSlope (fun (y : X) => ↑(f y)) x ≤ ↑K

The descending slope at x of a function that is K-Lipschitz on a neighbourhood of x is at most K.

theorem LipschitzWith.descendingSlope_le {X : Type u_1} [EMetricSpace X] {f : X → ℝ} {K : NNReal} (hf : LipschitzWith K f) (x : X) : TauCeti.descendingSlope (fun (y : X) => ↑(f y)) x ≤ ↑K

The descending slope of a K-Lipschitz function is at most K everywhere.

theorem TauCeti.descendingSlope_const_mul {X : Type u_1} [EMetricSpace X] {c : ℝ} (hc : 0 ≤ c) (f : X → ℝ) (x : X) : descendingSlope (fun (y : X) => ↑(c * f y)) x = ENNReal.ofReal c * descendingSlope (fun (y : X) => ↑(f y)) x

Scaling a real-valued function by c ≥ 0 scales its descending slope by c.

theorem TauCeti.descendingSlope_le_iSup {X : Type u_1} [MetricSpace X] (m : ℝ) (φ : X → EReal) (x : X) : descendingSlope φ x ≤ ⨆ (y : X), (φ x - φ y + ↑(m / 2 * dist x y ^ 2)).toENNReal / edist x y

The descending slope of any energy is at most its global slope sup_y (φ x - φ y + (m / 2) d(x, y)²)⁺ / d(x, y), for every m: near x the correction (m / 2) d(x, y) vanishes.

theorem HasFDerivAt.descendingSlope_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {x : E} (hf : HasFDerivAt f f' x) : TauCeti.descendingSlope (fun (y : E) => ↑(f y)) x = ‖f'‖ₑ

On a real normed space, the descending slope at x of a function with derivative f' at x is the norm of f': the function decreases fastest in the direction opposite to where f' is largest.

theorem HasDerivAt.descendingSlope_eq {g : ℝ → ℝ} {D t : ℝ} (hg : HasDerivAt g D t) : TauCeti.descendingSlope (fun (u : ℝ) => ↑(g u)) t = ‖D‖ₑ

The descending slope at t of a real function of a real variable with derivative D at t is |D|.