𝕜 : Type u_2
E : Type u_1
F : Type u_3
G : Type ?u.1537340
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 : ℝ≥0
k : ℕ
h : ↑‖x‖₊ < radius p
⊢ HasSum (fun l => ∑' (x_1 : { s // Finset.card s = l }), ‖p (k + l)‖₊ * ‖x‖₊ ^ l)
    (∑' (s : (l : ℕ) × { s // Finset.card s = l }), ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst)
𝕜 : Type u_2
E : Type u_1
F : Type u_3
G : Type ?u.1537340
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 : ℝ≥0
k : ℕ
h : ↑‖x‖₊ < radius p
⊢ ‖changeOrigin p x k‖₊ ≤ ∑' (s : (l : ℕ) × { s // Finset.card s = l }), ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst
refine' tsum_of_nnnorm_bounded _ fun l => p.nnnorm_changeOriginSeries_apply_le_tsum k l x
𝕜 : Type u_2
E : Type u_1
F : Type u_3
G : Type ?u.1537340
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 : ℝ≥0
k : ℕ
h : ↑‖x‖₊ < radius p
this : Summable fun s => ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst
⊢ HasSum (fun l => ∑' (x_1 : { s // Finset.card s = l }), ‖p (k + l)‖₊ * ‖x‖₊ ^ l)
    (∑' (s : (l : ℕ) × { s // Finset.card s = l }), ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst)
𝕜 : Type u_2
E : Type u_1
F : Type u_3
G : Type ?u.1537340
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 : ℝ≥0
k : ℕ
h : ↑‖x‖₊ < radius p
⊢ HasSum (fun l => ∑' (x_1 : { s // Finset.card s = l }), ‖p (k + l)‖₊ * ‖x‖₊ ^ l)
    (∑' (s : (l : ℕ) × { s // Finset.card s = l }), ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst)
have := p.changeOriginSeries_summable_aux₂ h k
𝕜 : Type u_2
E : Type u_1
F : Type u_3
G : Type ?u.1537340
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 : ℝ≥0
k : ℕ
h : ↑‖x‖₊ < radius p
this : Summable fun s => ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst
l : ℕ
⊢ HasSum (fun c => ‖p (k + { fst := l, snd := c }.fst)‖₊ * ‖x‖₊ ^ { fst := l, snd := c }.fst)
    (∑' (x_1 : { s // Finset.card s = l }), ‖p (k + l)‖₊ * ‖x‖₊ ^ l)
𝕜 : Type u_2
E : Type u_1
F : Type u_3
G : Type ?u.1537340
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 : ℝ≥0
k : ℕ
h : ↑‖x‖₊ < radius p
this : Summable fun s => ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst
⊢ HasSum (fun l => ∑' (x_1 : { s // Finset.card s = l }), ‖p (k + l)‖₊ * ‖x‖₊ ^ l)
    (∑' (s : (l : ℕ) × { s // Finset.card s = l }), ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst)
refine' HasSum.sigma this.hasSum fun l => _
no goals
𝕜 : Type u_2
E : Type u_1
F : Type u_3
G : Type ?u.1537340
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 : ℝ≥0
k : ℕ
h : ↑‖x‖₊ < radius p
this : Summable fun s => ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst
l : ℕ
⊢ HasSum (fun c => ‖p (k + { fst := l, snd := c }.fst)‖₊ * ‖x‖₊ ^ { fst := l, snd := c }.fst)
    (∑' (x_1 : { s // Finset.card s = l }), ‖p (k + l)‖₊ * ‖x‖₊ ^ l)
exact ((NNReal.summable_sigma.1 this).1 l).hasSum