English
If hN: ∞ ≤ N, then HasFTaylorSeriesUpTo N f p is equivalent to a conjunction: (i) ∀ x, (p x 0).curry0 = f x; (ii) ∀ m ∈ ℕ, ∀ x, HasFDerivAt (fun y => p y 0) (p x 1).curryLeft x; (iii) HasFTaylorSeriesUpTo n.cast (fun x => toFun (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x => (p x).shift).
Русский
Если hN: ∞ ≤ N, то HasFTaylorSeriesUpTo N f p эквивалентно сочетанию условий: нулевой коэффициент совпадает с f, для всех m∈ℕ и всех x имеет место fderivAt соответствующего коэффициента, и далее имеет место HasFTaylorSeriesUpTo для n.cast от преобразованной функции.
LaTeX
$$$\text{HasFTaylorSeriesUpTo } N f p \iff (\forall x, (p x 0).curry0 = f x) \land (\forall m \in \mathbb{N}, \forall x, HasFDerivAt (fun y \mapsto p y 0) (p x 1).curryLeft x) \land HasFTaylorSeriesUpTo n.cast (\lambda x => \text{toFunLike.coe} (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (\lambda x => (p x).shift)$$
Lean4
/-- In the case that `n = ∞` we don't need the continuity assumption in
`HasFTaylorSeriesUpTo`. -/
theorem hasFTaylorSeriesUpTo_top_iff' (hN : ∞ ≤ N) :
HasFTaylorSeriesUpTo N f p ↔
(∀ x, (p x 0).curry0 = f x) ∧ ∀ (m : ℕ) (x), HasFDerivAt (fun y => p y m) (p x m.succ).curryLeft x :=
by
simp only [← hasFTaylorSeriesUpToOn_univ_iff, hasFTaylorSeriesUpToOn_top_iff' hN, mem_univ, forall_true_left,
hasFDerivWithinAt_univ]
