English
There exists a bound on the remainder depending on a bound for the (n+1)-th derivative over the interval.
Русский
Существует граница остатка, зависящая от верхней оценки (n+1)-й производной на интервале.
LaTeX
$$$\\exists C, \\forall x \\in [a,b], \\|f(x) - taylorWithinEval f n (Icc a b) a x\\| \\le C \\frac{|x-a|^{n+1}}{n!}$$$
Lean4
/-- `(d/dx) lim_{n → ∞} f n x = lim_{n → ∞} f' n x` when the `f' n` converge
_uniformly_ to their limit at `x`.
In words the assumptions mean the following:
* `hf'`: The `f'` converge "uniformly at" `x` to `g'`. This does not mean that the `f' n` even
converge away from `x`!
* `hf`: For all `(y, n)` with `y` sufficiently close to `x` and `n` sufficiently large, `f' n` is
the derivative of `f n`
* `hfg`: The `f n` converge pointwise to `g` on a neighborhood of `x` -/
theorem hasFDerivAt_of_tendstoUniformlyOnFilter [NeBot l] (hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x))
(hf : ∀ᶠ n : ι × E in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2)
(hfg : ∀ᶠ y in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))) : HasFDerivAt g (g' x) x :=
by
letI : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
rw [hasFDerivAt_iff_tendsto]
-- Introduce extra quantifier via curried filters
suffices Tendsto (fun y : ι × E => ‖y.2 - x‖⁻¹ * ‖g y.2 - g x - (g' x) (y.2 - x)‖) (l.curry (𝓝 x)) (𝓝 0)
by
rw [Metric.tendsto_nhds] at this ⊢
intro ε hε
specialize this ε hε
rw [eventually_curry_iff] at this
simp only at this
exact
(eventually_const.mp this).mono
(by simp only [imp_self, forall_const])
-- With the new quantifier in hand, we can perform the famous `ε/3` proof. Specifically,
-- we will break up the limit (the difference functions minus the derivative go to 0) into 3:
-- * The difference functions of the `f n` converge *uniformly* to the difference functions
-- of the `g n`
-- * The `f' n` are the derivatives of the `f n`
-- * The `f' n` converge to `g'` at `x`
conv =>
congr
ext
rw [← abs_norm, ← abs_inv, ← @RCLike.norm_ofReal 𝕜 _ _, RCLike.ofReal_inv, ← norm_smul]
rw [← tendsto_zero_iff_norm_tendsto_zero]
have :
(fun a : ι × E => (‖a.2 - x‖⁻¹ : 𝕜) • (g a.2 - g x - (g' x) (a.2 - x))) =
((fun a : ι × E => (‖a.2 - x‖⁻¹ : 𝕜) • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a : ι × E =>
(‖a.2 - x‖⁻¹ : 𝕜) • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) +
fun a : ι × E => (‖a.2 - x‖⁻¹ : 𝕜) • (f' a.1 x - g' x) (a.2 - x) :=
by
ext; simp only [Pi.add_apply]; rw [← smul_add, ← smul_add]; congr
simp only [map_sub, sub_add_sub_cancel, ContinuousLinearMap.coe_sub', Pi.sub_apply]
abel
simp_rw [this]
have : 𝓝 (0 : G) = 𝓝 (0 + 0 + 0) := by simp only [add_zero]
rw [this]
refine Tendsto.add (Tendsto.add ?_ ?_) ?_
· have := difference_quotients_converge_uniformly hf' hf hfg
rw [Metric.tendstoUniformlyOnFilter_iff] at this
rw [Metric.tendsto_nhds]
intro ε hε
apply ((this ε hε).filter_mono curry_le_prod).mono
intro n hn
rw [dist_eq_norm] at hn ⊢
convert hn using 2
module
· -- (Almost) the definition of the derivatives
rw [Metric.tendsto_nhds]
intro ε hε
rw [eventually_curry_iff]
refine hf.curry.mono fun n hn => ?_
have := hn.self_of_nhds
rw [hasFDerivAt_iff_tendsto, Metric.tendsto_nhds] at this
refine (this ε hε).mono fun y hy => ?_
rw [dist_eq_norm] at hy ⊢
simp only [sub_zero, map_sub, norm_mul, norm_inv, norm_norm] at hy ⊢
rw [norm_smul, norm_inv, RCLike.norm_coe_norm]
exact hy
· -- hfg' after specializing to `x` and applying the definition of the operator norm
refine Tendsto.mono_left ?_ curry_le_prod
have h1 : Tendsto (fun n : ι × E => g' n.2 - f' n.1 n.2) (l ×ˢ 𝓝 x) (𝓝 0) :=
by
rw [Metric.tendstoUniformlyOnFilter_iff] at hf'
exact Metric.tendsto_nhds.mpr fun ε hε => by simpa using hf' ε hε
have h2 : Tendsto (fun n : ι => g' x - f' n x) l (𝓝 0) :=
by
rw [Metric.tendsto_nhds] at h1 ⊢
exact fun ε hε => (h1 ε hε).curry.mono fun n hn => hn.self_of_nhds
refine squeeze_zero_norm ?_ (tendsto_zero_iff_norm_tendsto_zero.mp (tendsto_fst.comp (h2.prodMap tendsto_id)))
intro n
simp_rw [norm_smul, norm_inv, RCLike.norm_coe_norm]
by_cases hx : x = n.2; · simp [hx]
have hnx : 0 < ‖n.2 - x‖ := by rw [norm_pos_iff]; intro hx'; exact hx (eq_of_sub_eq_zero hx').symm
rw [inv_mul_le_iff₀ hnx, mul_comm]
simp only [Function.comp_apply, Prod.map_apply']
rw [norm_sub_rev]
exact (f' n.1 x - g' x).le_opNorm (n.2 - x)
