English
Uniform bound on derivatives implies uniform Cauchy bounds for Taylor polynomials inside the ball around x.
Русский
Единый предел на производные внутри шара обеспечивает единообразное ограничение остатка Тейлора внутри шара.
LaTeX
$$$\\text{(complex expression in ball with bounds on derivatives)}$$$
Lean4
theorem uniformCauchySeqOn_ball_of_deriv {r : ℝ} (hf' : UniformCauchySeqOn f' l (Metric.ball x r))
(hf : ∀ n : ι, ∀ y : 𝕜, y ∈ Metric.ball x r → HasDerivAt (f n) (f' n y) y) (hfg : Cauchy (map (fun n => f n x) l)) :
UniformCauchySeqOn f l (Metric.ball x r) :=
by
simp_rw [hasDerivAt_iff_hasFDerivAt] at hf
rw [uniformCauchySeqOn_iff_uniformCauchySeqOnFilter] at hf'
have hf' : UniformCauchySeqOn (fun n => fun z => (1 : 𝕜 →L[𝕜] 𝕜).smulRight (f' n z)) l (Metric.ball x r) :=
by
rw [uniformCauchySeqOn_iff_uniformCauchySeqOnFilter]
exact hf'.one_smulRight
exact uniformCauchySeqOn_ball_of_fderiv hf' hf hfg
