-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem memℓp_gen {f : ∀ i, E i} (hf : Summable fun i => ‖f i‖ ^ p.toReal) : Memℓp f p

Proof state:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ p.toReal
hp : 0 < p.toReal
⊢ Memℓp f p

Tactic:
exact (memℓp_gen_iff hp).2 hf

Result:
no goals

Proof state:
case inl.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal 0
H : Summable fun x => 1
⊢ {i | f i ≠ 0}.Finite

Tactic:
exact (Set.Finite.of_summable_const (by norm_num) H).subset (Set.subset_univ _)

Result:
no goals

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ p.toReal
⊢ Memℓp f p

Tactic:
rcases p.trichotomy with (rfl | rfl | hp)

Result:
case inl
α : Type u_3
E : α → Type u_4
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_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ⊤.toReal
⊢ Memℓp f ⊤

case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ p.toReal
hp : 0 < p.toReal
⊢ Memℓp f p

Proof state:
case inr.inl.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ⊤.toReal
⊢ BddAbove (Set.range fun i => ‖f i‖)

Tactic:
have H : Summable fun _ : α => (1 : ℝ) := by simpa using hf

Result:
case inr.inl.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ⊤.toReal
H : Summable fun x => 1
⊢ BddAbove (Set.range fun i => ‖f i‖)

Proof state:
α : Type u_3
E : α → Type u_4
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

Tactic:
norm_num

Result:
no goals

Proof state:
case inr.inl.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ⊤.toReal
H : Summable fun x => 1
⊢ BddAbove (Set.range fun i => ‖f i‖)

Tactic:
simpa using ((Set.Finite.of_summable_const (by norm_num) H).image fun i => ‖f i‖).bddAbove

Result:
no goals

Proof state:
case inl.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal 0
⊢ {i | f i ≠ 0}.Finite

Tactic:
have H : Summable fun _ : α => (1 : ℝ) := by simpa using hf

Result:
case inl.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal 0
H : Summable fun x => 1
⊢ {i | f i ≠ 0}.Finite

Proof state:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal 0
⊢ Memℓp f 0

Tactic:
apply memℓp_zero

Result:
case inl.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal 0
⊢ {i | f i ≠ 0}.Finite

Proof state:
case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ⊤.toReal
⊢ Memℓp f ⊤

Tactic:
apply memℓp_infty

Result:
case inr.inl.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ⊤.toReal
⊢ BddAbove (Set.range fun i => ‖f i‖)

Proof state:
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal 0
⊢ Summable fun x => 1

Tactic:
simpa using hf

Result:
no goals

Proof state:
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ⊤.toReal
H : Summable fun x => 1
⊢ 0 < 1

Tactic:
norm_num

Result:
no goals

Proof state:
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i => ‖f i‖ ^ ⊤.toReal
⊢ Summable fun x => 1

Tactic:
simpa using hf

Result:
no goals