English
There exists a bound C such that for all nearby x, the difference f(x) − (P_n f)(x0, x) is bounded by C times the distance to x0 raised to power n+1.
Русский
Существует константа C такая, что для всех близких x разность f(x) − (P_n f)(x0, x) ≤ C dist(x,x0)^{n+1}.
LaTeX
$$$\\exists C, \\forall x \\in Icc a b, \\|f(x) - taylorWithinEval f n (Icc a b) a x\\| ≤ C \\cdot |x-a|^{n+1}$$$
Lean4
/-- If our derivatives converge uniformly, then the Fréchet derivatives converge uniformly -/
theorem one_smulRight {l' : Filter 𝕜} (hf' : UniformCauchySeqOnFilter f' l l') :
UniformCauchySeqOnFilter (fun n => fun z => (1 : 𝕜 →L[𝕜] 𝕜).smulRight (f' n z)) l l' := by
-- The tricky part of this proof is that operator norms are written in terms of `≤` whereas
-- metrics are written in terms of `<`. So we need to shrink `ε` utilizing the archimedean
-- property of `ℝ`
rw [SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero,
Metric.tendstoUniformlyOnFilter_iff] at hf' ⊢
intro ε hε
obtain ⟨q, hq, hq'⟩ := exists_between hε.lt
apply (hf' q hq).mono
intro n hn
refine lt_of_le_of_lt ?_ hq'
simp only [dist_eq_norm, Pi.zero_apply, zero_sub, norm_neg] at hn ⊢
refine ContinuousLinearMap.opNorm_le_bound _ hq.le ?_
intro z
simp only [ContinuousLinearMap.coe_sub', Pi.sub_apply, ContinuousLinearMap.smulRight_apply,
ContinuousLinearMap.one_apply]
rw [← smul_sub, norm_smul, mul_comm]
gcongr
