case inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ ‖0‖ = 0

case inr.inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ ‖0‖ = 0

case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < ENNReal.toReal p
⊢ ‖0‖ = 0
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ ‖0‖ = 0
rcases p.trichotomy with (rfl | rfl | hp)
no goals
case inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ ‖0‖ = 0
simp [lp.norm_eq_card_dsupport]
no goals
case inr.inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ ‖0‖ = 0
simp [lp.norm_eq_ciSup]
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < ENNReal.toReal p
⊢ (∑' (i : α), ‖↑0 i‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p) = 0
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < ENNReal.toReal p
⊢ ‖0‖ = 0
rw [lp.norm_eq_tsum_rpow hp]
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < ENNReal.toReal p
hp' : 1 / ENNReal.toReal p ≠ 0
⊢ (∑' (i : α), ‖↑0 i‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p) = 0
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < ENNReal.toReal p
⊢ (∑' (i : α), ‖↑0 i‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p) = 0
have hp' : 1 / p.toReal ≠ 0 := one_div_ne_zero hp.ne'
no goals
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < ENNReal.toReal p
hp' : 1 / ENNReal.toReal p ≠ 0
⊢ (∑' (i : α), ‖↑0 i‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p) = 0
simpa [Real.zero_rpow hp.ne'] using Real.zero_rpow hp'