Descending slope (metric slope) for real-valued energies on a (pseudo)metric space.

We use the right-neighborhood filter around x restricted to points at positive distance, nhdsWithin x {y | 0 < dist y x}, to avoid division by 0 in the pseudometric setting.

A helper set for points at positive distance from x.

def Frourio.posDist {X : Type u_1} [PseudoMetricSpace X] (x : X) : Set X

Equations

• Frourio.posDist x = {y : X | 0 < dist y x}

def Frourio.posPart (r : ℝ) : ℝ

Positive part of a real number, implemented as max r 0 (local helper).

Equations

• Frourio.posPart r = max r 0

@[simp]

theorem Frourio.posPart_nonneg (r : ℝ) : 0 ≤ posPart r

@[simp]

theorem Frourio.posPart_le_abs (r : ℝ) : posPart r ≤ |r|

noncomputable def Frourio.slopeQuot {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (x y : X) : ℝ

Local quotient used in the slope definition.

Equations

• Frourio.slopeQuot F x y = Frourio.posPart (F x - F y) / dist x y

theorem Frourio.slopeQuot_nonneg_of_posdist {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (x y : X) (h : 0 < dist x y) : 0 ≤ slopeQuot F x y

Pointwise nonnegativity of the slope quotient when the distance is positive.

noncomputable def Frourio.descendingSlopeE {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (x : X) : EReal

EReal descending slope |∂F|_E(x) = limsup_{y→x, 0<dist(y,x)} ((F x - F y)^+) / d(x,y). This EReal form is convenient when moving to Dini/EVI-style statements.

Equations

• Frourio.descendingSlopeE F x = Filter.limsup (fun (y : X) => ↑(Frourio.posPart (F x - F y) / dist x y)) (nhdsWithin x (Frourio.posDist x))

noncomputable def Frourio.descendingSlope {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (x : X) : ℝ

Real descending slope |∂F|(x) = limsup_{y→x, 0<dist(y,x)} ((F x - F y)^+) / d(x,y). We restrict to points at positive distance to avoid division by zero in PseudoMetricSpaces.

Equations

• Frourio.descendingSlope F x = Filter.limsup (fun (y : X) => Frourio.posPart (F x - F y) / dist x y) (nhdsWithin x (Frourio.posDist x))

theorem Frourio.eventually_nonneg_slopeQuot {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (x : X) : ∀ᶠ (y : X) in nhdsWithin x (posDist x), 0 ≤ posPart (F x - F y) / dist x y

theorem Frourio.descendingSlopeE_const {X : Type u_1} [PseudoMetricSpace X] (x : X) (c : ℝ) [(nhdsWithin x (posDist x)).NeBot] : descendingSlopeE (fun (x : X) => c) x = 0

Constant function: EReal descending slope is 0.

theorem Frourio.descendingSlope_const {X : Type u_1} [PseudoMetricSpace X] (x : X) (c : ℝ) [(nhdsWithin x (posDist x)).NeBot] : descendingSlope (fun (x : X) => c) x = 0

Constant function: real descending slope is 0.

Helper lemmas for limsup on real-valued functions

theorem Frourio.limsup_le_of_eventually_le_real {α : Type u_2} {l : Filter α} [l.NeBot] {f g : α → ℝ} (hf_lb : ∃ (m : ℝ), ∀ᶠ (a : α) in l, m ≤ f a) (hg_ub : ∃ (M : ℝ), ∀ᶠ (a : α) in l, g a ≤ M) (h : ∀ᶠ (a : α) in l, f a ≤ g a) : Filter.limsup f l ≤ Filter.limsup g l

If a real-valued function is eventually bounded below on a filter and is eventually ≤ another function that is bounded above, then the limsup is monotone with respect to ≤.

theorem Frourio.isCoboundedUnder_le_of_eventually_nonneg {α : Type u_2} {l : Filter α} [l.NeBot] {f : α → ℝ} (h : ∀ᶠ (a : α) in l, 0 ≤ f a) : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l f

Convenience: eventual nonnegativity implies a lower cobound for use with limsup_le_of_le on real-valued functions.

theorem Frourio.descendingSlopeE_le_of_lipschitzWith {X : Type u_1} [PseudoMetricSpace X] (K : ℝ) (_hK : 0 ≤ K) (F : X → ℝ) (x : X) (hL : ∀ (x y : X), dist (F x) (F y) ≤ K * dist x y) : descendingSlopeE F x ≤ ↑K

Final Lipschitz bound (EReal): descendingSlopeE F x ≤ K when F is K‑Lipschitz.