English
If the order N is at least infinity, then having a Taylor series up to N is equivalent to having Taylor series up to all orders n+k for every natural number n, for a fixed k.
Русский
Если порядок N удовлетворяет N≥∞, то наличие ряда Тейлора до N эквивалентно существованию ряда Тейлора до всех порядков n+k для каждого натурального n при фиксированном k.
LaTeX
$$$$\text{HasFTaylorSeriesUpToOn}(N,f,p,s) \iff \forall n\in\mathbb{N}, \text{HasFTaylorSeriesUpToOn}(n+k,f,p,s).$$$$
Lean4
theorem hasFTaylorSeriesUpToOn_top_iff_add (hN : ∞ ≤ N) (k : ℕ) :
HasFTaylorSeriesUpToOn N f p s ↔ ∀ n : ℕ, HasFTaylorSeriesUpToOn (n + k : ℕ) f p s :=
by
constructor
· intro H n
apply H.of_le (natCast_le_of_coe_top_le_withTop hN _)
· intro H
constructor
· exact (H 0).zero_eq
· intro m _
apply (H m.succ).fderivWithin m (by norm_cast; cutsat)
· intro m _
apply (H m).cont m (by simp)
