English
Over the reals, a continuously differentiable function is strictly differentiable.
Русский
По вещественным числам непрерывно дифференцируемая функция является строго дифференцируемой.
LaTeX
$$$$ \text{Strict differentiability of } f $$$$
Lean4
/-- If `(f y - f x) / (y - x)` converges to a limit as `y` tends to `x`, then the same goes if
`y` is shifted a little bit, i.e., `f (y + (y-x)^2) - f x) / (y - x)` converges to the same limit.
This lemma contains a slightly more general version of this statement (where one considers
convergence along some subfilter, typically `𝓝[<] x` or `𝓝[>] x`) tailored to the application
to almost everywhere differentiability of monotone functions. -/
theorem tendsto_apply_add_mul_sq_div_sub {f : ℝ → ℝ} {x a c d : ℝ} {l : Filter ℝ} (hl : l ≤ 𝓝[≠] x)
(hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)) (h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l) :
Tendsto (fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)) l (𝓝 a) :=
by
have L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1) :=
by
have : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 (1 + c * (x - x))) :=
by
apply Tendsto.mono_left _ (hl.trans nhdsWithin_le_nhds)
exact ((tendsto_id.sub_const x).const_mul c).const_add 1
simp only [_root_.sub_self, add_zero, mul_zero] at this
apply Tendsto.congr' (Eventually.filter_mono hl _) this
filter_upwards [self_mem_nhdsWithin] with y hy
field_simp [sub_ne_zero.2 hy]
ring
have Z := (hf.comp h').mul L
rw [mul_one] at Z
apply Tendsto.congr' _ Z
have : ∀ᶠ y in l, y + c * (y - x) ^ 2 ≠ x := by apply Tendsto.mono_right h' hl self_mem_nhdsWithin
filter_upwards [this] with y hy
simp [field, sub_ne_zero.2 hy]
