English
If HasFTaylorSeriesUpToOn N f p s holds, then for every m, and every x in s, the m-th derivative relation holds pointwise: p x m.succ yields a derivative of p x m.
Русский
Если HasFTaylorSeriesUpToOn N f p s выполняется, то для каждого m и каждого x∈s выполняется точечное отношение: p x m.succ является производной p x m.
LaTeX
$$$$\text{HasFTaylorSeriesUpToOn}(N,f,p,s) \Rightarrow \forall m\in\mathbb{N}, \forall x\in s, \text{HasFDerivWithinAt}( (\lambda y, p(y,m)) , p(x,m.succ).\text{curryLeft}, s, x).$$$$
Lean4
/-- In the case that `n = ∞` we don't need the continuity assumption in
`HasFTaylorSeriesUpToOn`. -/
theorem hasFTaylorSeriesUpToOn_top_iff' (hN : ∞ ≤ N) :
HasFTaylorSeriesUpToOn N f p s ↔
(∀ x ∈ s, (p x 0).curry0 = f x) ∧
∀ m : ℕ, ∀ x ∈ s, HasFDerivWithinAt (fun y => p y m) (p x m.succ).curryLeft s x :=
by
-- Everything except for the continuity is trivial:
refine
⟨fun h => ⟨h.1, fun m => h.2 m (natCast_lt_of_coe_top_le_withTop hN _)⟩, fun h =>
⟨h.1, fun m _ => h.2 m,
fun m _ x hx =>
-- The continuity follows from the existence of a derivative:
(h.2 m x hx).continuousWithinAt⟩⟩
