English
If ∑ ‖p_n‖ r^n converges for every r, then the radius is ∞.
Русский
Если сумма сходится для каждого r, то радиус бесконечен.
LaTeX
$$$\\forall r, \\; Summable( n \\mapsto \\|p_n\\| r^n ) \\Rightarrow p.radius = \\infty.$$$
Lean4
@[simp]
theorem radius_shift (p : FormalMultilinearSeries 𝕜 E F) : p.shift.radius = p.radius :=
by
simp only [radius, shift, Nat.succ_eq_add_one, ContinuousMultilinearMap.curryRight_norm]
congr
ext r
apply eq_of_le_of_ge
· apply iSup_mono'
intro C
use ‖p 0‖ ⊔ (C * r)
apply iSup_mono'
intro h
simp only [le_refl, le_sup_iff, exists_prop, and_true]
intro n
rcases n with - | m
· simp
right
rw [pow_succ, ← mul_assoc]
gcongr; apply h
· apply iSup_mono'
intro C
use ‖p 1‖ ⊔ C / r
apply iSup_mono'
intro h
simp only [le_refl, le_sup_iff, exists_prop, and_true]
intro n
cases eq_zero_or_pos r with
| inl hr =>
rw [hr]
cases n <;> simp
| inr hr =>
right
rw [← NNReal.coe_pos] at hr
specialize h (n + 1)
rw [le_div_iff₀ hr]
rwa [pow_succ, ← mul_assoc] at h
