English
The derivative series of p is the formal multilinear series obtained by currying the first argument and composing with the origin-change series for k = 1. It encodes the derivative of the original series when it exists.
Русский
Ряд производной p получается из p, пропуская первый аргумент и композиционируя с p.changeOrigin при k=1; он кодирует производную исходного ряда, если она существует.
LaTeX
$$$p.derivSeries = (\\text{continuousMultilinearCurryFin1 } p) \\circ_{\\text{FMS}} (p.changeOriginSeries 1)$$$
Lean4
/-- The radius of convergence of `p.changeOrigin x` is at least `p.radius - ‖x‖`. In other words,
`p.changeOrigin x` is well defined on the largest ball contained in the original ball of
convergence. -/
theorem changeOrigin_radius : p.radius - ‖x‖₊ ≤ (p.changeOrigin x).radius :=
by
refine ENNReal.le_of_forall_pos_nnreal_lt fun r _h0 hr => ?_
rw [lt_tsub_iff_right, add_comm] at hr
have hr' : (‖x‖₊ : ℝ≥0∞) < p.radius := (le_add_right le_rfl).trans_lt hr
apply le_radius_of_summable_nnnorm
have (k : ℕ) :
‖p.changeOrigin x k‖₊ * r ^ k ≤
(∑' s : Σ l : ℕ, { s : Finset (Fin (k + l)) // s.card = l }, ‖p (k + s.1)‖₊ * ‖x‖₊ ^ s.1) * r ^ k :=
by gcongr; exact p.nnnorm_changeOrigin_le k hr'
refine NNReal.summable_of_le this ?_
simpa only [← NNReal.tsum_mul_right] using (NNReal.summable_sigma.1 (p.changeOriginSeries_summable_aux₁ hr)).2
