English
The zero-derivative iteratedFDerivWithin is equal to f composed with the inverse of the 0-th curry map.
Русский
Нулевой производной является тождество, что iteratedFDerivWithin 0 f s равен композиции f с обратной к 0-му раскатку карте.
LaTeX
$$$$\text{iteratedFDerivWithin}(\mathbb{k},0,f,s) = (\text{continuousMultilinearCurryFin0 }\mathbb{k} E F)^{-1} \circ 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`. Version for `n : WithTop ℕ∞`. -/
theorem hasFTaylorSeriesUpToOn_succ_iff_right :
HasFTaylorSeriesUpToOn (n + 1) f p s ↔
(∀ x ∈ s, (p x 0).curry0 = f x) ∧
(∀ x ∈ s, HasFDerivWithinAt (fun y => p y 0) (p x 1).curryLeft s x) ∧
HasFTaylorSeriesUpToOn n (fun x => continuousMultilinearCurryFin1 𝕜 E F (p x 1)) (fun x => (p x).shift) s :=
by
match n with
| ⊤ => exact hasFTaylorSeriesUpToOn_top_iff_right (by simp)
| (⊤ : ℕ∞) => exact hasFTaylorSeriesUpToOn_top_iff_right (by simp)
| (n : ℕ) => exact hasFTaylorSeriesUpToOn_succ_nat_iff_right
