English
There exists a bound C such that for all x in [a,b], the remainder is bounded by C (x−a)^{n+1}/n!, given a global bound on the (n+1)th derivative.
Русский
Существует константа C, такая что для всех x в [a,b] остаток не выше C (x−a)^{n+1}/n!, если (n+1)-я производная ограничена сверху на [a,b].
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
/-- A variant of the second fundamental theorem of calculus (FTC-2): If a sequence of functions
between real or complex normed spaces are differentiable on a ball centered at `x`, they
form a Cauchy sequence _at_ `x`, and their derivatives are Cauchy uniformly on the ball, then the
functions form a uniform Cauchy sequence on the ball.
NOTE: The fact that we work on a ball is typically all that is necessary to work with power series
and Dirichlet series (our primary use case). However, this can be generalized by replacing the ball
with any connected, bounded, open set and replacing uniform convergence with local uniform
convergence. See `cauchy_map_of_uniformCauchySeqOn_fderiv`.
-/
theorem uniformCauchySeqOn_ball_of_fderiv {r : ℝ} (hf' : UniformCauchySeqOn f' l (Metric.ball x r))
(hf : ∀ n : ι, ∀ y : E, y ∈ Metric.ball x r → HasFDerivAt (f n) (f' n y) y)
(hfg : Cauchy (map (fun n => f n x) l)) : UniformCauchySeqOn f l (Metric.ball x r) :=
by
letI : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
letI : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 _
have : NeBot l := (cauchy_map_iff.1 hfg).1
rcases le_or_gt r 0 with (hr | hr)
·
simp only [Metric.ball_eq_empty.2 hr, UniformCauchySeqOn, Set.mem_empty_iff_false, IsEmpty.forall_iff,
eventually_const, imp_true_iff]
rw [SeminormedAddGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_zero] at hf' ⊢
suffices
TendstoUniformlyOn (fun (n : ι × ι) (z : E) => f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0 (l ×ˢ l)
(Metric.ball x r) ∧
TendstoUniformlyOn (fun (n : ι × ι) (_ : E) => f n.1 x - f n.2 x) 0 (l ×ˢ l) (Metric.ball x r)
by
have := this.1.add this.2
rw [add_zero] at this
refine this.congr ?_
filter_upwards with n z _ using (by simp)
constructor
· -- This inequality follows from the mean value theorem
rw [Metric.tendstoUniformlyOn_iff] at hf' ⊢
intro ε hε
obtain ⟨q, hqpos, hq⟩ : ∃ q : ℝ, 0 < q ∧ q * r < ε :=
by
simp_rw [mul_comm]
exact exists_pos_mul_lt hε.lt r
apply (hf' q hqpos.gt).mono
intro n hn y hy
simp_rw [dist_eq_norm, Pi.zero_apply, zero_sub, norm_neg] at hn ⊢
have mvt :=
Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le
(fun z hz => ((hf n.1 z hz).sub (hf n.2 z hz)).hasFDerivWithinAt) (fun z hz => (hn z hz).le) (convex_ball x r)
(Metric.mem_ball_self hr) hy
refine lt_of_le_of_lt mvt ?_
have : q * ‖y - x‖ < q * r :=
mul_lt_mul' rfl.le (by simpa only [dist_eq_norm] using Metric.mem_ball.mp hy) (norm_nonneg _) hqpos
exact this.trans hq
· -- This is just `hfg` run through `eventually_prod_iff`
refine Metric.tendstoUniformlyOn_iff.mpr fun ε hε => ?_
obtain ⟨t, ht, ht'⟩ := (Metric.cauchy_iff.mp hfg).2 ε hε
rw [eventually_prod_iff]
refine ⟨fun n => f n x ∈ t, ht, fun n => f n x ∈ t, ht, ?_⟩
intro n hn n' hn' z _
rw [dist_eq_norm, Pi.zero_apply, zero_sub, norm_neg, ← dist_eq_norm]
exact ht' _ hn _ hn'
