English
If a function has a finite power series on a ball, then its derivative has a corresponding power series with index decreased by one.
Русский
Если функция имеет конечное разложение по ФПС в шаре, то ее производная имеет соответствующее разложение со смещением индекса на единицу назад.
LaTeX
$$$HasFiniteFPowerSeriesOnBall f p x (n+1) r \Rightarrow HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x n r$$$
Lean4
/-- If a function has a finite power series on a ball, then so does its derivative.
This is a variant of `HasFiniteFPowerSeriesOnBall.fderiv` where the degree of `f` is `< n`
and not `< n + 1`. -/
theorem fderiv' (h : HasFiniteFPowerSeriesOnBall f p x n r) :
HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x (n - 1) r :=
by
obtain rfl | hn := eq_or_ne n 0
· rw [zero_tsub]
refine HasFiniteFPowerSeriesOnBall.bound_zero_of_eq_zero (fun y hy ↦ ?_) h.r_pos fun n ↦ ?_
· rw [Filter.EventuallyEq.fderiv_eq (f := fun _ ↦ 0)]
· simp
·
exact
Filter.eventuallyEq_iff_exists_mem.mpr
⟨EMetric.ball x r, EMetric.isOpen_ball.mem_nhds hy, fun z hz ↦ by rw [h.eq_zero_of_bound_zero z hz]⟩
· apply ContinuousMultilinearMap.ext; intro a
change (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOriginSeries 1 n a) = 0
rw [p.changeOriginSeries_finite_of_finite h.finite 1 (Nat.zero_le _)]
exact map_zero _
· rw [← Nat.succ_pred hn] at h
exact h.fderiv
