English
If HasFTaylorSeriesUpTo n f p holds with hn: 1 ≤ n, then f is differentiable everywhere in the field 𝕜.
Русский
Если функция имеет ряд Тейлора до порядка n≥1, то она дифференцируема в каждой точке.
LaTeX
$$$\text{HasFTaylorSeriesUpTo } n f p \;\Rightarrow\; \text{Differentiable } 𝕜\, f$$
Lean4
/-- `p` is a Taylor series of `f` up to `n+1` if and only if `p.shift` is a Taylor series up to `n`
for `p 1`, which is a derivative of `f`. -/
theorem hasFTaylorSeriesUpTo_succ_nat_iff_right {n : ℕ} :
HasFTaylorSeriesUpTo (n + 1 : ℕ) f p ↔
(∀ x, (p x 0).curry0 = f x) ∧
(∀ x, HasFDerivAt (fun y => p y 0) (p x 1).curryLeft x) ∧
HasFTaylorSeriesUpTo n (fun x => continuousMultilinearCurryFin1 𝕜 E F (p x 1)) fun x => (p x).shift :=
by
simp only [hasFTaylorSeriesUpToOn_succ_nat_iff_right, ← hasFTaylorSeriesUpToOn_univ_iff, mem_univ, forall_true_left,
hasFDerivWithinAt_univ]
