α : 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 }
⊢ (∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p * ENNReal.toReal p) =
    ∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p

case hx
α : 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 }
⊢ 0 ≤ ∑' (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 }
⊢ ‖f‖ ^ ENNReal.toReal p = ∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p
rw [norm_eq_tsum_rpow hp, ← Real.rpow_mul]
case hx.h
α : 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 }
⊢ ∀ (i : α), 0 ≤ ‖↑f i‖ ^ ENNReal.toReal p
case hx
α : 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 }
⊢ 0 ≤ ∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p
apply tsum_nonneg
case hx.h
α : 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 }
i : α
⊢ 0 ≤ ‖↑f i‖ ^ ENNReal.toReal p
case hx.h
α : 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 }
⊢ ∀ (i : α), 0 ≤ ‖↑f i‖ ^ ENNReal.toReal p
intro i
no goals
case hx.h
α : 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 }
i : α
⊢ 0 ≤ ‖↑f i‖ ^ ENNReal.toReal p
calc
  (0 : ℝ) = (0 : ℝ) ^ p.toReal := by rw [Real.zero_rpow hp.ne']
  _ ≤ _ := Real.rpow_le_rpow rfl.le (norm_nonneg (f i)) hp.le
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 }
⊢ (∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p * ENNReal.toReal p) =
    ∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p
field_simp [hp.ne']
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 }
i : α
⊢ 0 = 0 ^ ENNReal.toReal p
rw [Real.zero_rpow hp.ne']