English
If HasDerivWithinAt f f' (Ici x) x, then liminf of slope on nhdsWithin x to the right is ≤ ‖f'‖.
Русский
Если имеется производная внутри на [x, ∞), лиминф наклона справа не превышает ‖f'‖.
LaTeX
$$hf : HasDerivWithinAt f f' (Ici x) x → hr : ‖f'‖ < r → ∃ᶠ z in 𝓝[>] x, (z - x)⁻¹ * (‖f z - f x‖) < r$$
Lean4
/-- 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‖`. -/
theorem liminf_right_slope_norm_le (hf : HasDerivWithinAt f f' (Ici x) x) (hr : ‖f'‖ < r) :
∃ᶠ z in 𝓝[>] x, (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r :=
by
have := (hf.Ioi_of_Ici.limsup_slope_norm_le hr).frequently
refine this.mp (Eventually.mono self_mem_nhdsWithin fun z hxz hz ↦ ?_)
rwa [Real.norm_eq_abs, abs_of_pos (sub_pos_of_lt hxz)] at hz
