English
If f has a derivative within a set along a filter, then the limit along the filter of a scaled difference quotient converges to the derivative evaluated at the tangent vector.
Русский
Если имеется производная внутри множества вдоль фильтра, предел масштабированного приращения стремится к производной в касательном направлении.
LaTeX
$$$\text{limit } \frac{f(x+d_n)-f(x)-f'(d_n)}{\|d_n\|} \to 0$, yielding the tangent limit.$$
Lean4
/-- If a function f has a derivative f' at x, a rescaled version of f around x converges to f',
i.e., `n (f (x + (1/n) v) - f x)` converges to `f' v`. More generally, if `c n` tends to infinity
and `c n * d n` tends to `v`, then `c n * (f (x + d n) - f x)` tends to `f' v`. This lemma expresses
this fact, for functions having a derivative within a set. Its specific formulation is useful for
tangent cone related discussions. -/
theorem lim (h : HasFDerivWithinAt f f' s x) {α : Type*} (l : Filter α) {c : α → 𝕜} {d : α → E} {v : E}
(dtop : ∀ᶠ n in l, x + d n ∈ s) (clim : Tendsto (fun n => ‖c n‖) l atTop)
(cdlim : Tendsto (fun n => c n • d n) l (𝓝 v)) : Tendsto (fun n => c n • (f (x + d n) - f x)) l (𝓝 (f' v)) :=
by
have tendsto_arg : Tendsto (fun n => x + d n) l (𝓝[s] x) :=
by
conv in 𝓝[s] x => rw [← add_zero x]
rw [nhdsWithin, tendsto_inf]
constructor
· apply tendsto_const_nhds.add (tangentConeAt.lim_zero l clim cdlim)
· rwa [tendsto_principal]
have : (fun y => f y - f x - f' (y - x)) =o[𝓝[s] x] fun y => y - x := h.isLittleO
have : (fun n => f (x + d n) - f x - f' (x + d n - x)) =o[l] fun n => x + d n - x := this.comp_tendsto tendsto_arg
have : (fun n => f (x + d n) - f x - f' (d n)) =o[l] d := by simpa only [add_sub_cancel_left]
have : (fun n => c n • (f (x + d n) - f x - f' (d n))) =o[l] fun n => c n • d n :=
(isBigO_refl c l).smul_isLittleO this
have : (fun n => c n • (f (x + d n) - f x - f' (d n))) =o[l] fun _ => (1 : ℝ) :=
this.trans_isBigO (cdlim.isBigO_one ℝ)
have L1 : Tendsto (fun n => c n • (f (x + d n) - f x - f' (d n))) l (𝓝 0) := (isLittleO_one_iff ℝ).1 this
have L2 : Tendsto (fun n => f' (c n • d n)) l (𝓝 (f' v)) := Tendsto.comp f'.cont.continuousAt cdlim
have L3 : Tendsto (fun n => c n • (f (x + d n) - f x - f' (d n)) + f' (c n • d n)) l (𝓝 (0 + f' v)) := L1.add L2
have : (fun n => c n • (f (x + d n) - f x - f' (d n)) + f' (c n • d n)) = fun n => c n • (f (x + d n) - f x) :=
by
ext n
simp [smul_sub]
rwa [this, zero_add] at L3
