English
For top order, HasFTaylorSeriesUpToOn N f p s is equivalent to HasFTaylorSeriesUpToOn N of the shifted data with the last term appropriately aligned.
Русский
Для верхнего порядка HasFTaylorSeriesUpToOn N f p s эквивалентно HasFTaylorSeriesUpToOn N для сдвинутых данных с корректной выровкой последних членов.
LaTeX
$$$$\text{HasFTaylorSeriesUpToOn}(N,f,p,s) \iff \Big(\forall x\in s, (p x 0).curry0 = f x\Big) \land \Big(\forall x\in s, HasFDerivWithinAt (\lambda y, p y 0) (p x 1).curryLeft s x\Big) \land \text{HasFTaylorSeriesUpToOn}(N (\lambda x, \text{continuousMultilinearCurryFin1}(p x 1)) , (\lambda x, (p x).shift), s\Big).$$$$
Lean4
/-- `p` is a Taylor series of `f` up to `⊤` if and only if `p.shift` is a Taylor series up to `⊤`
for `p 1`, which is a derivative of `f`. -/
theorem hasFTaylorSeriesUpToOn_top_iff_right (hN : ∞ ≤ N) :
HasFTaylorSeriesUpToOn N 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
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· rw [hasFTaylorSeriesUpToOn_top_iff_add hN 1] at h
rw [hasFTaylorSeriesUpToOn_top_iff hN]
exact
⟨(hasFTaylorSeriesUpToOn_succ_nat_iff_right.1 (h 1)).1, (hasFTaylorSeriesUpToOn_succ_nat_iff_right.1 (h 1)).2.1,
fun n ↦ (hasFTaylorSeriesUpToOn_succ_nat_iff_right.1 (h n)).2.2⟩
· apply (hasFTaylorSeriesUpToOn_top_iff_add hN 1).2 (fun n ↦ ?_)
rw [hasFTaylorSeriesUpToOn_succ_nat_iff_right]
exact ⟨h.1, h.2.1, (h.2.2).of_le (m := n) (natCast_le_of_coe_top_le_withTop hN n)⟩
