English
If HasDerivWithinAt f f' s x then for any r > ‖f'‖, ∀ᶠ z in nhdsWithin x, slope_norm f x z < r.
Русский
Если внутри есть производная, то существует окрестность, где норма наклона меньше любого r выше нормы производной.
LaTeX
$$hf : HasDerivWithinAt f f' s x → hr : ‖f'‖ < r → ∀ᶠ z in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r$$
Lean4
/-- If `f` has derivative `f'` within `s` at `x`, then for any `r > ‖f'‖` the ratio
`(‖f z‖ - ‖f x‖) / ‖z - x‖` is less than `r` in some neighborhood of `x` within `s`.
In other words, the limit superior of this ratio as `z` tends to `x` along `s`
is less than or equal to `‖f'‖`.
This lemma is a weaker version of `HasDerivWithinAt.limsup_norm_slope_le`
where `‖f z‖ - ‖f x‖` is replaced by `‖f z - f x‖`. -/
theorem limsup_slope_norm_le (hf : HasDerivWithinAt f f' s x) (hr : ‖f'‖ < r) :
∀ᶠ z in 𝓝[s] x, ‖z - x‖⁻¹ * (‖f z‖ - ‖f x‖) < r :=
by
apply (hf.limsup_norm_slope_le hr).mono
intro z hz
refine lt_of_le_of_lt (mul_le_mul_of_nonneg_left (norm_sub_norm_le _ _) ?_) hz
exact inv_nonneg.2 (norm_nonneg _)
