English
Taylor remainder bounds for derivatives of analytic functions: for HasFPowerSeriesWithinAt f p s x, the sub-derivative remainder f(x+y) - p(1)(y) is Big-O of ‖y‖^n near y = 0.
Русский
Ограничения остатка Тейлора для аналитических функций: при HasFPowerSeriesWithinAt f p s x остаток f(x+y) − p(1)(y) является Big-O по ‖y‖^n при y → 0.
LaTeX
$$$\forall n\in\mathbb{N},\; \bigl(f(x+y) - p.partialSum\,n\,y\bigr) =O\bigl(\|y\|^n\bigr) \text{ as } y \to 0\,.$$$
Lean4
/-- Taylor formula for an analytic function within a set, `IsBigO` version. -/
theorem isBigO_sub_partialSum_pow (hf : HasFPowerSeriesWithinAt f p s x) (n : ℕ) :
(fun y : E => f (x + y) - p.partialSum n y) =O[𝓝[(x + ·) ⁻¹' insert x s] 0] fun y => ‖y‖ ^ n :=
by
rcases hf with ⟨r, hf⟩
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 hf.r_pos with ⟨r', r'0, h⟩
obtain ⟨a, -, C, -, hp⟩ :
∃ a ∈ Ioo (0 : ℝ) 1,
∃ C > 0,
∀ y ∈ Metric.ball (0 : E) r',
∀ n, x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / r')) ^ n :=
hf.uniform_geometric_approx' h
refine isBigO_iff.2 ⟨C * (a / r') ^ n, ?_⟩
replace r'0 : 0 < (r' : ℝ) := mod_cast r'0
filter_upwards [inter_mem_nhdsWithin _ (Metric.ball_mem_nhds (0 : E) r'0)] with y hy
simpa [mul_pow, mul_div_assoc, mul_assoc, div_mul_eq_mul_div, div_pow] using hp y hy.2 n (by simpa using hy.1)
