case inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal 0
⊢ Memℓp f 0

case inr.inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal ⊤
⊢ Memℓp f ⊤

case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal p
hp : 0 < ENNReal.toReal p
⊢ Memℓp f p
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal p
⊢ Memℓp f p
rcases p.trichotomy with (rfl | rfl | hp)
no goals
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal p
hp : 0 < ENNReal.toReal p
⊢ Memℓp f p
exact (memℓp_gen_iff hp).2 hf
case inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal 0
⊢ Set.Finite {i | f i ≠ 0}
case inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal 0
⊢ Memℓp f 0
apply memℓp_zero
case inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal 0
H : Summable fun x => 1
⊢ Set.Finite {i | f i ≠ 0}
case inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal 0
⊢ Set.Finite {i | f i ≠ 0}
have H : Summable fun _ : α => (1 : ℝ) := by simpa using hf
no goals
case inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal 0
H : Summable fun x => 1
⊢ Set.Finite {i | f i ≠ 0}
exact (Set.Finite.of_summable_const (by norm_num) H).subset (Set.subset_univ _)
no goals
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal 0
⊢ Summable fun x => 1
simpa using hf
no goals
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal 0
H : Summable fun x => 1
⊢ 0 < 1
norm_num
case inr.inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal ⊤
⊢ BddAbove (Set.range fun i => ‖f i‖)
case inr.inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal ⊤
⊢ Memℓp f ⊤
apply memℓp_infty
case inr.inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal ⊤
H : Summable fun x => 1
⊢ BddAbove (Set.range fun i => ‖f i‖)
case inr.inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal ⊤
⊢ BddAbove (Set.range fun i => ‖f i‖)
have H : Summable fun _ : α => (1 : ℝ) := by simpa using hf
no goals
case inr.inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal ⊤
H : Summable fun x => 1
⊢ BddAbove (Set.range fun i => ‖f i‖)
simpa using ((Set.Finite.of_summable_const (by norm_num) H).image fun i => ‖f i‖).bddAbove
no goals
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal ⊤
⊢ Summable fun x => 1
simpa using hf
no goals
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal ⊤
H : Summable fun x => 1
⊢ 0 < 1
norm_num