English
Under standard differentiability assumptions on a real interval [a,b], there exists x' ∈ (a,b) such that the remainder has the Lagrange form with (x−a)^{n+1} in the numerator.
Русский
При стандартных условиях дифференцируемости на промежутке [a,b] существует x'∈(a,b), для которого остаток имеет форму Лагранжа с (x−a)^{n+1} в числителе.
LaTeX
$$$\\exists x' \\in (a,b), \\ f(x) - P_n(f)(a,x) = \\dfrac{f^{(n+1)}(x') (x-a)^{n+1}}{(n+1)!}$$$
Lean4
/-- If a sequence of functions between real or complex normed spaces are differentiable on a
preconnected open set, they form a Cauchy sequence _at_ `x`, and their derivatives are Cauchy
uniformly on the set, then the functions form a Cauchy sequence at any point in the set. -/
theorem cauchy_map_of_uniformCauchySeqOn_fderiv {s : Set E} (hs : IsOpen s) (h's : IsPreconnected s)
(hf' : UniformCauchySeqOn f' l s) (hf : ∀ n : ι, ∀ y : E, y ∈ s → HasFDerivAt (f n) (f' n y) y) {x₀ x : E}
(hx₀ : x₀ ∈ s) (hx : x ∈ s) (hfg : Cauchy (map (fun n => f n x₀) l)) : Cauchy (map (fun n => f n x) l) :=
by
have : NeBot l := (cauchy_map_iff.1 hfg).1
let t := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
suffices H : s ⊆ t from (H hx).2
have A : ∀ x ε, x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t := fun x ε xt hx y hy =>
⟨hx hy, (uniformCauchySeqOn_ball_of_fderiv (hf'.mono hx) (fun n y hy => hf n y (hx hy)) xt.2).cauchy_map hy⟩
have open_t : IsOpen t := by
rw [Metric.isOpen_iff]
intro x hx
rcases Metric.isOpen_iff.1 hs x hx.1 with ⟨ε, εpos, hε⟩
exact ⟨ε, εpos, A x ε hx hε⟩
have st_nonempty : (s ∩ t).Nonempty := ⟨x₀, hx₀, ⟨hx₀, hfg⟩⟩
suffices H : closure t ∩ s ⊆ t from h's.subset_of_closure_inter_subset open_t st_nonempty H
rintro x ⟨xt, xs⟩
obtain ⟨ε, εpos, hε⟩ : ∃ (ε : ℝ), ε > 0 ∧ Metric.ball x ε ⊆ s := Metric.isOpen_iff.1 hs x xs
obtain ⟨y, yt, hxy⟩ : ∃ (y : E), y ∈ t ∧ dist x y < ε / 2 := Metric.mem_closure_iff.1 xt _ (half_pos εpos)
have B : Metric.ball y (ε / 2) ⊆ Metric.ball x ε := by apply Metric.ball_subset_ball'; rw [dist_comm]; linarith
exact A y (ε / 2) yt (B.trans hε) (Metric.mem_ball.2 hxy)
