radius_unshift — Mathlib

English

If ∑ ‖p_n‖ r^n converges, then for any x with ∥x∥ ≤ r, the series ∑ ‖p_n(x)‖ converges.

Русский

Если ∑ ‖p_n‖ r^n сходится, то для каждого x с ∥x∥ ≤ r сумма ∑ ‖p_n(x)‖ сходится.

LaTeX

$$$\\text{If } \\sum_n \\|p_n\\| r^n < \\infty, \\text{ then } \\sum_n \\|p_n(x)\\| < \\infty \\text{ for } \\|x\\| \\le r.$$$

Lean4

@[simp]
theorem radius_unshift (p : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)) (z : F) : (p.unshift z).radius = p.radius := by
  rw [← radius_shift, unshift_shift]

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