English
If HasDerivWithinAt f f' s x, then for every r > ‖f'‖, eventually ‖z - x‖⁻¹*(‖f z‖ - ‖f x‖) < r for z in nhdsWithin.
Русский
Если есть производная внутри, для любого ограничителя r больше нормы производной, близко к x внутри s, выражение меньше 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'‖`. -/
theorem limsup_norm_slope_le (hf : HasDerivWithinAt f f' s x) (hr : ‖f'‖ < r) :
∀ᶠ z in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r :=
by
have hr₀ : 0 < r := lt_of_le_of_lt (norm_nonneg f') hr
have A : ∀ᶠ z in 𝓝[s \ { x }] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r :=
(hasDerivWithinAt_iff_tendsto_slope.1 hf).norm (IsOpen.mem_nhds isOpen_Iio hr)
have B : ∀ᶠ z in 𝓝[{ x }] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r :=
mem_of_superset self_mem_nhdsWithin (singleton_subset_iff.2 <| by simp [hr₀])
have C := mem_sup.2 ⟨A, B⟩
rw [← nhdsWithin_union, diff_union_self, nhdsWithin_union, mem_sup] at C
filter_upwards [C.1]
simp only [norm_smul, mem_Iio, norm_inv]
exact fun _ => id
