English
If HasFTaylorSeriesUpToOn (n+1) f p s holds, then HasFTaylorSeriesUpToOn n (fun x => continuousMultilinearCurryFin1 𝕜 E F (p x 1)) (fun x => (p x).shift) s holds.
Русский
Если HasFTaylorSeriesUpToOn (n+1) f p s, то HasFTaylorSeriesUpToOn n (функция x → continuousMultilinearCurryFin1( p x 1)) и HasFTaylorSeriesUpToOn (fun x → (p x).shift) на s.
LaTeX
$$$$\text{HasFTaylorSeriesUpToOn}(n+1,f,p,s) \Rightarrow \text{HasFTaylorSeriesUpToOn}n\big( x \mapsto \text{continuousMultilinearCurryFin1}(p x 1) , x \mapsto (p x).shift, s\big).$$$$
Lean4
theorem shift_of_succ {n : ℕ} (H : HasFTaylorSeriesUpToOn (n + 1 : ℕ) f p s) :
(HasFTaylorSeriesUpToOn n (fun x => continuousMultilinearCurryFin1 𝕜 E F (p x 1)) (fun x => (p x).shift)) s :=
by
constructor
· intro x _
rfl
· intro m (hm : (m : WithTop ℕ∞) < n) x (hx : x ∈ s)
have A : (m.succ : WithTop ℕ∞) < n.succ := by
rw [Nat.cast_lt] at hm ⊢
exact Nat.succ_lt_succ hm
change
HasFDerivWithinAt (continuousMultilinearCurryRightEquiv' 𝕜 m E F ∘ (p · m.succ))
(p x m.succ.succ).curryRight.curryLeft s x
rw [(continuousMultilinearCurryRightEquiv' 𝕜 m E F).comp_hasFDerivWithinAt_iff']
convert H.fderivWithin _ A x hx
ext y v
change p x (m + 2) (snoc (cons y (init v)) (v (last _))) = p x (m + 2) (cons y v)
rw [← cons_snoc_eq_snoc_cons, snoc_init_self]
· intro m (hm : (m : WithTop ℕ∞) ≤ n)
suffices A : ContinuousOn (p · (m + 1)) s from
(continuousMultilinearCurryRightEquiv' 𝕜 m E F).continuous.comp_continuousOn A
refine H.cont _ ?_
rw [Nat.cast_le] at hm ⊢
exact Nat.succ_le_succ hm
