English
If the scaled norms converge to a limit along atTop to l, then r ≤ radius.
Русский
Если предел подстроенных норм сходится к l вдоль atTop, то r ≤ radius.
LaTeX
$$$\\text{If } \\text{Tendsto}(n \\mapsto \\|p_n\\| \\cdot r^n)_{n\\to\\infty} \\to \\mathcal{N},\\; \\text{then } r ≤ p.radius.$$$
Lean4
/-- The radius of the sum of two formal series is at least the minimum of their two radii. -/
theorem min_radius_le_radius_add (p q : FormalMultilinearSeries 𝕜 E F) : min p.radius q.radius ≤ (p + q).radius :=
by
refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_
rw [lt_min_iff] at hr
have := ((p.isLittleO_one_of_lt_radius hr.1).add (q.isLittleO_one_of_lt_radius hr.2)).isBigO
refine (p + q).le_radius_of_isBigO ((isBigO_of_le _ fun n => ?_).trans this)
rw [← add_mul, norm_mul, norm_mul, norm_norm]
gcongr
exact (norm_add_le _ _).trans (le_abs_self _)
