α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p ∧ p < ⊤
f : (i : α) → E i
⊢ Memℓp f 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 : (i : α) → E i
⊢ Memℓp f p ↔ Summable fun i => ‖f i‖ ^ ENNReal.toReal p
rw [ENNReal.toReal_pos_iff] at hp
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p ∧ p < ⊤
f : (i : α) → E i
⊢ (if p = 0 then Set.Finite {i | ¬f i = 0}
    else if p = ⊤ then BddAbove (Set.range fun i => ‖f i‖) else Summable fun i => ‖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 < p ∧ p < ⊤
f : (i : α) → E i
⊢ Memℓp f p ↔ Summable fun i => ‖f i‖ ^ ENNReal.toReal p
dsimp [Memℓp]
no goals
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p ∧ p < ⊤
f : (i : α) → E i
⊢ (if p = 0 then Set.Finite {i | ¬f i = 0}
    else if p = ⊤ then BddAbove (Set.range fun i => ‖f i‖) else Summable fun i => ‖f i‖ ^ ENNReal.toReal p) ↔
    Summable fun i => ‖f i‖ ^ ENNReal.toReal p
rw [if_neg hp.1.ne', if_neg hp.2.ne]