Theorems · Theorem · real analysis

HasDerivWithinAt.liminf_right_slope_norm_le

∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {f' : E} {x r : ℝ},
  HasDerivWithinAt f f' (Set.Ici x) x →
    ‖f'‖ < r → ∃ᶠ (z : ℝ) in nhdsWithin x (Set.Ioi x), (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r

If f has derivative f' within (x, +∞) at x, then for any r > ‖f'‖ the ratio (‖f z‖ - ‖f x‖) / (z - x) is frequently less than r as z → x+0. In other words, the limit inferior of this ratio as z tends to x+0 is less than or equal to ‖f'‖. See also * HasDerivWithinAt.limsup_norm_slope_le for a stronger version using limit superior and any set s; * HasDerivWithinAt.liminf_right_norm_slope_le for a stronger version using ‖f z - f xp‖ instead of ‖f z‖ - ‖f x‖.

Defined in

Mathlib.Analysis.Calculus.Deriv.Slope

Cited by

3 results in Mathlib

Foundations

Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace