English
Taylor's theorem: the difference between f and its Taylor approximation taylorWithinEval is little-o of (x−x0)^n as x approaches x0 from inside s.
Русский
Теорема Тейлора: разность между f и её аппроксимацией Тейлора taylorWithinEval ведет себя как маленькое o по отношению к (x−x0)^n при x, стремящемся к x0 внутри s.
LaTeX
$$$f(x) - taylorWithinEval\ f\ n\ s\ x_0\ x = o_{\mathcal{N}(s) x_0}\bigl((x - x_0)^n\bigr)$$$
Lean4
/-- **Taylor's theorem** using little-o notation. -/
theorem taylor_isLittleO {f : ℝ → E} {x₀ : ℝ} {n : ℕ} {s : Set ℝ} (hs : Convex ℝ s) (hx₀s : x₀ ∈ s)
(hf : ContDiffOn ℝ n f s) : (fun x ↦ f x - taylorWithinEval f n s x₀ x) =o[𝓝[s] x₀] fun x ↦ (x - x₀) ^ n := by
induction n generalizing f with
| zero =>
simp only [taylor_within_zero_eval, pow_zero, Asymptotics.isLittleO_one_iff]
rw [tendsto_sub_nhds_zero_iff]
exact hf.continuousOn.continuousWithinAt hx₀s
| succ n h =>
rcases s.eq_singleton_or_nontrivial hx₀s with rfl | hs'
· simp
replace hs' := uniqueDiffOn_convex hs (hs.nontrivial_iff_nonempty_interior.1 hs')
simp only [Nat.cast_add, Nat.cast_one] at hf
convert
Convex.isLittleO_pow_succ_real hs hx₀s ?_ (h (hf.derivWithin hs' le_rfl)) (f := fun x ↦
f x - taylorWithinEval f (n + 1) s x₀ x) using
1
· simp
· intro x hx
refine HasDerivWithinAt.sub ?_ (hasDerivAt_taylorWithinEval_succ f n).hasDerivWithinAt
exact (hf.differentiableOn le_add_self _ hx).hasDerivWithinAt
