α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
⊢ HasSum (fun i => ‖↑f i‖ ^ ENNReal.toReal p) (∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p)
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
⊢ HasSum (fun i => ‖↑f i‖ ^ ENNReal.toReal p) (‖f‖ ^ ENNReal.toReal p)
rw [norm_rpow_eq_tsum hp]
no goals
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < ENNReal.toReal p
f : { x // x ∈ lp E p }
⊢ HasSum (fun i => ‖↑f i‖ ^ ENNReal.toReal p) (∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p)
exact ((lp.memℓp f).summable hp).hasSum