English
There is a point x' with a Cauchy-type remainder for iterated derivatives.
Русский
Существует точка x' с остатком в форме типа Коши для итеративных производных.
LaTeX
$$$\\exists x' \\in Ioo(x_0,x), \\\\ f(x) - taylorWithinEval f n (Icc x_0 x) x_0 x = iteratedDerivWithin (n+1) f (Icc x_0 x) x' \\cdot \\frac{(x - x')^{n} (x - x_0)}{n!}$$$
Lean4
/-- A slight variant of `hasFDerivAt_of_tendstoLocallyUniformlyOn` with the assumption stated
in terms of `DifferentiableOn` rather than `HasFDerivAt`. This makes a few proofs nicer in
complex analysis where holomorphicity is assumed but the derivative is not known a priori. -/
theorem hasFDerivAt_of_tendsto_locally_uniformly_on' [NeBot l] {s : Set E} (hs : IsOpen s)
(hf' : TendstoLocallyUniformlyOn (fderiv 𝕜 ∘ f) g' l s) (hf : ∀ n, DifferentiableOn 𝕜 (f n) s)
(hfg : ∀ x ∈ s, Tendsto (fun n => f n x) l (𝓝 (g x))) (hx : x ∈ s) : HasFDerivAt g (g' x) x :=
by
refine hasFDerivAt_of_tendstoLocallyUniformlyOn hs hf' (fun n z hz => ?_) hfg hx
exact ((hf n z hz).differentiableAt (hs.mem_nhds hz)).hasFDerivAt
