𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.211235
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
x : E
hx : ↑‖x‖₊ < radius p
⊢ Summable fun n => ‖↑(p n) fun x_1 => x‖
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.211235
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
x : E
hx : x ∈ EMetric.ball 0 (radius p)
⊢ Summable fun n => ‖↑(p n) fun x_1 => x‖
rw [mem_emetric_ball_zero_iff] at hx
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.211235
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
x : E
hx : ↑‖x‖₊ < radius p
n : ℕ
⊢ ‖p n‖ * ∏ i : Fin n, ‖x‖ = ‖p n‖ * ↑‖x‖₊ ^ n
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.211235
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
x : E
hx : ↑‖x‖₊ < radius p
⊢ Summable fun n => ‖↑(p n) fun x_1 => x‖
refine' summable_of_nonneg_of_le
  (fun _ => norm_nonneg _) (fun n => ((p n).le_op_norm _).trans_eq _) (p.summable_norm_mul_pow hx)
no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.211235
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
x : E
hx : ↑‖x‖₊ < radius p
n : ℕ
⊢ ‖p n‖ * ∏ i : Fin n, ‖x‖ = ‖p n‖ * ↑‖x‖₊ ^ n
simp