English
There exists x' ∈ Ioo x0 x such that f(x) − (P_n f)(x0, x) equals f^{(n+1)}(x') (x−x')^n (x−x0)/n!, i.e., a Cauchy form of the remainder.
Русский
Существует x' между x0 и x, такое что остаток Тейлора принимает форму Коши: остаток равен f^{(n+1)}(x') (x−x')^n (x−x0)/n!.
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
/-- If a sequence of functions real or complex functions are eventually differentiable on a
neighborhood of `x`, they are Cauchy _at_ `x`, and their derivatives
are a uniform Cauchy sequence in a neighborhood of `x`, then the functions form a uniform Cauchy
sequence in a neighborhood of `x`. -/
theorem uniformCauchySeqOnFilter_of_fderiv (hf' : UniformCauchySeqOnFilter f' l (𝓝 x))
(hf : ∀ᶠ n : ι × E in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2) (hfg : Cauchy (map (fun n => f n x) l)) :
UniformCauchySeqOnFilter f l (𝓝 x) :=
by
letI : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
letI : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 _
rw [SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero] at hf' ⊢
suffices
TendstoUniformlyOnFilter (fun (n : ι × ι) (z : E) => f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0 (l ×ˢ l) (𝓝 x) ∧
TendstoUniformlyOnFilter (fun (n : ι × ι) (_ : E) => f n.1 x - f n.2 x) 0 (l ×ˢ l) (𝓝 x)
by
have := this.1.add this.2
rw [add_zero] at this
exact this.congr (by simp)
constructor
· -- This inequality follows from the mean value theorem. To apply it, we will need to shrink our
-- neighborhood to small enough ball
rw [Metric.tendstoUniformlyOnFilter_iff] at hf' ⊢
intro ε hε
have := (tendsto_swap4_prod.eventually (hf.prod_mk hf)).diag_of_prod_right
obtain ⟨a, b, c, d, e⟩ := eventually_prod_iff.1 ((hf' ε hε).and this)
obtain ⟨R, hR, hR'⟩ := Metric.nhds_basis_ball.eventually_iff.mp d
let r := min 1 R
have hr : 0 < r := by simp [r, hR]
have hr' : ∀ ⦃y : E⦄, y ∈ Metric.ball x r → c y := fun y hy =>
hR' (lt_of_lt_of_le (Metric.mem_ball.mp hy) (min_le_right _ _))
have hxy : ∀ y : E, y ∈ Metric.ball x r → ‖y - x‖ < 1 :=
by
intro y hy
rw [Metric.mem_ball, dist_eq_norm] at hy
exact lt_of_lt_of_le hy (min_le_left _ _)
have hxyε : ∀ y : E, y ∈ Metric.ball x r → ε * ‖y - x‖ < ε :=
by
intro y hy
exact
(mul_lt_iff_lt_one_right hε.lt).mpr
(hxy y hy)
-- With a small ball in hand, apply the mean value theorem
refine
eventually_prod_iff.mpr
⟨_, b, fun e : E => Metric.ball x r e, eventually_mem_set.mpr (Metric.nhds_basis_ball.mem_of_mem hr),
fun {n} hn {y} hy => ?_⟩
simp only [Pi.zero_apply, dist_zero_left] at e ⊢
refine lt_of_le_of_lt ?_ (hxyε y hy)
exact
Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le
(fun y hy => ((e hn (hr' hy)).2.1.sub (e hn (hr' hy)).2.2).hasFDerivWithinAt) (fun y hy => (e hn (hr' hy)).1.le)
(convex_ball x r) (Metric.mem_ball_self hr) hy
· -- This is just `hfg` run through `eventually_prod_iff`
refine Metric.tendstoUniformlyOnFilter_iff.mpr fun ε hε => ?_
obtain ⟨t, ht, ht'⟩ := (Metric.cauchy_iff.mp hfg).2 ε hε
exact
eventually_prod_iff.mpr
⟨fun n : ι × ι => f n.1 x ∈ t ∧ f n.2 x ∈ t,
eventually_prod_iff.mpr ⟨_, ht, _, ht, fun {n} hn {n'} hn' => ⟨hn, hn'⟩⟩, fun _ => True, by simp,
fun {n} hn {y} _ => by simpa [norm_sub_rev, dist_eq_norm] using ht' _ hn.1 _ hn.2⟩
