radius_le_radius_derivSeries — Mathlib

English

The radius of convergence of p is at most the radius of the derivative series, with equality possible in general, since the derivative operation does not decrease the radius.

Русский

Радиус сходимости p не меньше радиуса ряда производной; в общем случае возможно равенство, поскольку операция производной не уменьшает радиус.

LaTeX

$$$p.radius \\le p.derivSeries.radius$$$

Lean4

theorem radius_le_radius_derivSeries : p.radius ≤ p.derivSeries.radius :=
  by
  apply (p.le_changeOriginSeries_radius 1).trans (radius_le_of_le (fun n ↦ ?_))
  apply (ContinuousLinearMap.norm_compContinuousMultilinearMap_le _ _).trans
  apply mul_le_of_le_one_left (norm_nonneg _)
  exact ContinuousLinearMap.opNorm_le_bound _ zero_le_one (by simp)

Похожие утверждения