𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1521843
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x y : E
r✝ R r : ℝ≥0
hr : ↑r < radius p
k n : ℕ
⊢ ‖changeOriginSeries p k n‖₊ * r ^ n ≤
    ∑' (y : { s // Finset.card s = n }), ‖p (k + { fst := n, snd := y }.fst)‖₊ * r ^ { fst := n, snd := y }.fst
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1521843
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x y : E
r✝ R r : ℝ≥0
hr : ↑r < radius p
k : ℕ
⊢ Summable fun l => ‖changeOriginSeries p k l‖₊ * r ^ l
refine' NNReal.summable_of_le
  (fun n => _) (NNReal.summable_sigma.1 <| p.changeOriginSeries_summable_aux₂ hr k).2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1521843
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x y : E
r✝ R r : ℝ≥0
hr : ↑r < radius p
k n : ℕ
⊢ ‖changeOriginSeries p k n‖₊ * r ^ n ≤ (∑' (x : { s // Finset.card s = n }), ‖p (k + n)‖₊) * r ^ n
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1521843
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x y : E
r✝ R r : ℝ≥0
hr : ↑r < radius p
k n : ℕ
⊢ ‖changeOriginSeries p k n‖₊ * r ^ n ≤
    ∑' (y : { s // Finset.card s = n }), ‖p (k + { fst := n, snd := y }.fst)‖₊ * r ^ { fst := n, snd := y }.fst
simp only [NNReal.tsum_mul_right]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.1521843
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x y : E
r✝ R r : ℝ≥0
hr : ↑r < radius p
k n : ℕ
⊢ ‖changeOriginSeries p k n‖₊ * r ^ n ≤ (∑' (x : { s // Finset.card s = n }), ‖p (k + n)‖₊) * r ^ n
exact mul_le_mul' (p.nnnorm_changeOriginSeries_le_tsum _ _) le_rfl