case mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.244081
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
⊢ radius p = ⊤ → ∀ (r : ℝ≥0), Summable fun n => ‖p n‖ * ↑r ^ n

case mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.244081
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
⊢ (∀ (r : ℝ≥0), Summable fun n => ‖p n‖ * ↑r ^ n) → radius p = ⊤
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.244081
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
⊢ radius p = ⊤ ↔ ∀ (r : ℝ≥0), Summable fun n => ‖p n‖ * ↑r ^ n
constructor
case mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.244081
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r✝ : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
h : radius p = ⊤
r : ℝ≥0
⊢ Summable fun n => ‖p n‖ * ↑r ^ n
case mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.244081
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
⊢ radius p = ⊤ → ∀ (r : ℝ≥0), Summable fun n => ‖p n‖ * ↑r ^ n
intro h r
case mp.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.244081
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r✝ : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
h : radius p = ⊤
r : ℝ≥0
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hp : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n
⊢ Summable fun n => ‖p n‖ * ↑r ^ n
case mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.244081
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r✝ : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
h : radius p = ⊤
r : ℝ≥0
⊢ Summable fun n => ‖p n‖ * ↑r ^ n
obtain ⟨a, ha : a ∈ Ioo (0 : ℝ) 1, C, - : 0 < C, hp⟩ := p.norm_mul_pow_le_mul_pow_of_lt_radius
  (show (r : ℝ≥0∞) < p.radius from h.symm ▸ ENNReal.coe_lt_top)
case mp.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.244081
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r✝ : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
h : radius p = ⊤
r : ℝ≥0
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hp : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n
n : ℕ
⊢ ‖‖p n‖ * ↑r ^ n‖ ≤ (fun n => C * a ^ n) n
case mp.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.244081
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r✝ : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
h : radius p = ⊤
r : ℝ≥0
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hp : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n
⊢ Summable fun n => ‖p n‖ * ↑r ^ n
refine' summable_of_norm_bounded
  (fun n => (C : ℝ) * a ^ n) ((summable_geometric_of_lt_1 ha.1.le ha.2).mul_left _) fun n => _
case mp.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.244081
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r✝ : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
h : radius p = ⊤
r : ℝ≥0
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
n : ℕ
hp : ‖p n‖ * ↑r ^ n ≤ C * a ^ n
⊢ ‖‖p n‖ * ↑r ^ n‖ ≤ (fun n => C * a ^ n) n
case mp.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.244081
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r✝ : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
h : radius p = ⊤
r : ℝ≥0
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hp : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n
n : ℕ
⊢ ‖‖p n‖ * ↑r ^ n‖ ≤ (fun n => C * a ^ n) n
specialize hp n
no goals
case mp.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.244081
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r✝ : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
h : radius p = ⊤
r : ℝ≥0
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
n : ℕ
hp : ‖p n‖ * ↑r ^ n ≤ C * a ^ n
⊢ ‖‖p n‖ * ↑r ^ n‖ ≤ (fun n => C * a ^ n) n
rwa [Real.norm_of_nonneg (mul_nonneg (norm_nonneg _) (pow_nonneg r.coe_nonneg n))]
no goals
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.244081
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p✝ : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
p : FormalMultilinearSeries 𝕜 E F
⊢ (∀ (r : ℝ≥0), Summable fun n => ‖p n‖ * ↑r ^ n) → radius p = ⊤
exact p.radius_eq_top_of_summable_norm