α : 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 }
s : Finset α
⊢ ∑ i in s, ‖↑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 }
s : Finset α
⊢ ∑ i in s, ‖↑f i‖ ^ ENNReal.toReal p ≤ ‖f‖ ^ ENNReal.toReal p
rw [lp.norm_rpow_eq_tsum hp f]
α : 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 }
s : Finset α
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ ENNReal.toReal p
⊢ ∑ i in s, ‖↑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 }
s : Finset α
⊢ ∑ i in s, ‖↑f i‖ ^ ENNReal.toReal p ≤ ∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p
have : ∀ i, 0 ≤ ‖f i‖ ^ p.toReal := fun i => Real.rpow_nonneg_of_nonneg (norm_nonneg _) _
α : 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 }
s : Finset α
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ ENNReal.toReal p
⊢ Summable fun 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 }
s : Finset α
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ ENNReal.toReal p
⊢ ∑ i in s, ‖↑f i‖ ^ ENNReal.toReal p ≤ ∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p
refine' sum_le_tsum _ (fun i _ => this i) _
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 }
s : Finset α
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ ENNReal.toReal p
⊢ Summable fun i => ‖↑f i‖ ^ ENNReal.toReal p
exact (lp.memℓp f).summable hp