English
If HasFTaylorSeriesUpToOn (n+1) f p s holds, then HasFTaylorSeriesUpToOn n f p s holds with a shift in data and derivative relation.
Русский
Если имеет место HasFTaylorSeriesUpToOn (n+1) f p s, то HasFTaylorSeriesUpToOn n f p s сохраняется с сдвигом данных и соотношением производных.
LaTeX
$$$$\text{HasFTaylorSeriesUpToOn}(n+1,f,p,s) \iff \text{HasFTaylorSeriesUpToOn}(n,f,p,s) \land\Big( \forall x\in s, HasFDerivWithinAt (f, p x n)\text{ и т. д.} \Big).$$$$
Lean4
/-- The `n`-th derivative of a function along a set, defined inductively by saying that the `n+1`-th
derivative of `f` is the derivative of the `n`-th derivative of `f` along this set, together with
an uncurrying step to see it as a multilinear map in `n+1` variables..
-/
noncomputable def iteratedFDerivWithin (n : ℕ) (f : E → F) (s : Set E) : E → E [×n]→L[𝕜] F :=
Nat.recOn n (fun x => ContinuousMultilinearMap.uncurry0 𝕜 E (f x)) fun _ rec x =>
ContinuousLinearMap.uncurryLeft (fderivWithin 𝕜 rec s x)
