English
For HasFPowerSeriesWithinOnBall hf, the derivative-increment difference f(y)-f(z)-p(1)(y-z) is bounded by a constant times max norms times the distance ‖y−z‖, uniformly on small balls around (x,x).
Русский
Для HasFPowerSeriesWithinOnBall hf разность f(y)−f(z)−p(1)(y−z) ограничена константой, умноженной на максимум норм между y и x и между z и x, и на ‖y−z‖, однозначно в малых шарах вокруг (x,x).
LaTeX
$$$\\exists C,\\; \\forall^{\\!} y,z \\;\\text{в} \\;\\mathrm{EMetric.ball}(x,r')\\;\\text{и} \\; y,z \\in \\mathrm{insert}\\,x\,s:\\; \\|f(y) - f(z) - p(1)(y-z)\\| \\le C \\cdot \\max\\|y-x\\| \\|z-x\\| \\cdot \\|y-z\\|$$$
Lean4
/-- Taylor formula for an analytic function, `IsBigO` version. -/
theorem isBigO_sub_partialSum_pow (hf : HasFPowerSeriesAt f p x) (n : ℕ) :
(fun y : E => f (x + y) - p.partialSum n y) =O[𝓝 0] fun y => ‖y‖ ^ n :=
by
rw [← hasFPowerSeriesWithinAt_univ] at hf
simpa using hf.isBigO_sub_partialSum_pow n
