Taylor remainder estimates obtained by integration along a contained segment, with explicit operator and coordinate Hessian bounds.
theorem
KamProject.Arnold1963.norm_taylor_remainder_le
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedSpace ℂ E]
[IsScalarTower ℝ ℂ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedSpace ℂ F]
[IsScalarTower ℝ ℂ F]
[CompleteSpace F]
{f : E → F}
{U : Set E}
{a b : E}
{C : ℝ}
(hab : segment ℝ a b ⊆ U)
(hf : AnalyticOnNhd ℂ f U)
(hC : NormBoundOn (fderiv ℂ (fderiv ℂ f)) U C)
:
theorem
KamProject.Arnold1963.norm_taylor_remainder_le_of_coordinate_bound
{n : ℕ}
{f : ComplexSpace n → ℂ}
{U : Set (ComplexSpace n)}
{a b : ComplexSpace n}
{Θ : ℝ}
(hab : segment ℝ a b ⊆ U)
(hf : AnalyticOnNhd ℂ f U)
(hΘ : 0 ≤ Θ)
(hbound : ∀ x ∈ U, ∀ (i j : Fin n), ‖((fderiv ℂ (fderiv ℂ f) x) (Pi.single i 1)) (Pi.single j 1)‖ ≤ Θ)
: