case inl.intro
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ 0
⊢ Memℓp f 0

case inr.inl.intro
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ⊤
⊢ Memℓp f ⊤

case inr.inr.inl.intro
α : Type u_1
E : α → Type u_2
p✝ q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < ENNReal.toReal p
hfq : Memℓp f 0
hpq : 0 ≤ p
⊢ Memℓp f p

case inr.inr.inr.inl.intro
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f ⊤
hpq : ⊤ ≤ ⊤
⊢ Memℓp f ⊤

case inr.inr.inr.inr.inl.intro
α : Type u_1
E : α → Type u_2
p q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < ENNReal.toReal q
hpq : q ≤ ⊤
⊢ Memℓp f ⊤

case inr.inr.inr.inr.inr.intro.intro
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
⊢ Memℓp f p
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
⊢ Memℓp f p
rcases ENNReal.trichotomy₂ hpq with
  (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, hp⟩ | ⟨rfl, rfl⟩ | ⟨hq, rfl⟩ | ⟨hq, _, hpq'⟩)
no goals
case inl.intro
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ 0
⊢ Memℓp f 0
exact hfq
case inr.inl.intro.hf
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ⊤
⊢ BddAbove (Set.range fun i => ‖f i‖)
case inr.inl.intro
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ⊤
⊢ Memℓp f ⊤
apply memℓp_infty
case inr.inl.intro.hf.intro
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ⊤
C : ℝ
hC : C ∈ upperBounds ((fun i => ‖f i‖) '' {i | f i ≠ 0})
⊢ BddAbove (Set.range fun i => ‖f i‖)
case inr.inl.intro.hf
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ⊤
⊢ BddAbove (Set.range fun i => ‖f i‖)
obtain ⟨C, hC⟩ := (hfq.finite_dsupport.image fun i => ‖f i‖).bddAbove
case inr.inl.intro.hf.intro
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ⊤
C : ℝ
hC : C ∈ upperBounds ((fun i => ‖f i‖) '' {i | f i ≠ 0})
⊢ max 0 C ∈ upperBounds (Set.range fun i => ‖f i‖)
case inr.inl.intro.hf.intro
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ⊤
C : ℝ
hC : C ∈ upperBounds ((fun i => ‖f i‖) '' {i | f i ≠ 0})
⊢ BddAbove (Set.range fun i => ‖f i‖)
use max 0 C
case inr.inl.intro.hf.intro.intro
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ⊤
C : ℝ
hC : C ∈ upperBounds ((fun i => ‖f i‖) '' {i | f i ≠ 0})
i : α
⊢ (fun i => ‖f i‖) i ≤ max 0 C
case inr.inl.intro.hf.intro
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ⊤
C : ℝ
hC : C ∈ upperBounds ((fun i => ‖f i‖) '' {i | f i ≠ 0})
⊢ max 0 C ∈ upperBounds (Set.range fun i => ‖f i‖)
rintro x ⟨i, rfl⟩
case pos
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ⊤
C : ℝ
hC : C ∈ upperBounds ((fun i => ‖f i‖) '' {i | f i ≠ 0})
i : α
hi : f i = 0
⊢ (fun i => ‖f i‖) i ≤ max 0 C

case neg
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ⊤
C : ℝ
hC : C ∈ upperBounds ((fun i => ‖f i‖) '' {i | f i ≠ 0})
i : α
hi : ¬f i = 0
⊢ (fun i => ‖f i‖) i ≤ max 0 C
case inr.inl.intro.hf.intro.intro
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ⊤
C : ℝ
hC : C ∈ upperBounds ((fun i => ‖f i‖) '' {i | f i ≠ 0})
i : α
⊢ (fun i => ‖f i‖) i ≤ max 0 C
by_cases hi : f i = 0
no goals
case pos
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ⊤
C : ℝ
hC : C ∈ upperBounds ((fun i => ‖f i‖) '' {i | f i ≠ 0})
i : α
hi : f i = 0
⊢ (fun i => ‖f i‖) i ≤ max 0 C
simp [hi]
no goals
case neg
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ⊤
C : ℝ
hC : C ∈ upperBounds ((fun i => ‖f i‖) '' {i | f i ≠ 0})
i : α
hi : ¬f i = 0
⊢ (fun i => ‖f i‖) i ≤ max 0 C
exact (hC ⟨i, hi, rfl⟩).trans (le_max_right _ _)
case inr.inr.inl.intro.hf
α : Type u_1
E : α → Type u_2
p✝ q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < ENNReal.toReal p
hfq : Memℓp f 0
hpq : 0 ≤ p
⊢ Summable fun i => ‖f i‖ ^ ENNReal.toReal p
case inr.inr.inl.intro
α : Type u_1
E : α → Type u_2
p✝ q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < ENNReal.toReal p
hfq : Memℓp f 0
hpq : 0 ≤ p
⊢ Memℓp f p
apply memℓp_gen
case inr.inr.inl.intro.hf
α : Type u_1
E : α → Type u_2
p✝ q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < ENNReal.toReal p
hfq : Memℓp f 0
hpq : 0 ≤ p
this : ∀ (i : α), ¬i ∈ Set.Finite.toFinset (_ : Set.Finite {i | f i ≠ 0}) → ‖f i‖ ^ ENNReal.toReal p = 0
⊢ Summable fun i => ‖f i‖ ^ ENNReal.toReal p
case inr.inr.inl.intro.hf
α : Type u_1
E : α → Type u_2
p✝ q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < ENNReal.toReal p
hfq : Memℓp f 0
hpq : 0 ≤ p
⊢ Summable fun i => ‖f i‖ ^ ENNReal.toReal p
have : ∀ (i) (_ : i ∉ hfq.finite_dsupport.toFinset), ‖f i‖ ^ p.toReal = 0 := by
  intro i hi
  have : f i = 0 := by simpa using hi
  simp [this, Real.zero_rpow hp.ne']
no goals
case inr.inr.inl.intro.hf
α : Type u_1
E : α → Type u_2
p✝ q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < ENNReal.toReal p
hfq : Memℓp f 0
hpq : 0 ≤ p
this : ∀ (i : α), ¬i ∈ Set.Finite.toFinset (_ : Set.Finite {i | f i ≠ 0}) → ‖f i‖ ^ ENNReal.toReal p = 0
⊢ Summable fun i => ‖f i‖ ^ ENNReal.toReal p
exact summable_of_ne_finset_zero this
α : Type u_1
E : α → Type u_2
p✝ q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < ENNReal.toReal p
hfq : Memℓp f 0
hpq : 0 ≤ p
i : α
hi : ¬i ∈ Set.Finite.toFinset (_ : Set.Finite {i | f i ≠ 0})
⊢ ‖f i‖ ^ ENNReal.toReal p = 0
α : Type u_1
E : α → Type u_2
p✝ q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < ENNReal.toReal p
hfq : Memℓp f 0
hpq : 0 ≤ p
⊢ ∀ (i : α), ¬i ∈ Set.Finite.toFinset (_ : Set.Finite {i | f i ≠ 0}) → ‖f i‖ ^ ENNReal.toReal p = 0
intro i hi
α : Type u_1
E : α → Type u_2
p✝ q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < ENNReal.toReal p
hfq : Memℓp f 0
hpq : 0 ≤ p
i : α
hi : ¬i ∈ Set.Finite.toFinset (_ : Set.Finite {i | f i ≠ 0})
this : f i = 0
⊢ ‖f i‖ ^ ENNReal.toReal p = 0
α : Type u_1
E : α → Type u_2
p✝ q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < ENNReal.toReal p
hfq : Memℓp f 0
hpq : 0 ≤ p
i : α
hi : ¬i ∈ Set.Finite.toFinset (_ : Set.Finite {i | f i ≠ 0})
⊢ ‖f i‖ ^ ENNReal.toReal p = 0
have : f i = 0 := by simpa using hi
no goals
α : Type u_1
E : α → Type u_2
p✝ q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < ENNReal.toReal p
hfq : Memℓp f 0
hpq : 0 ≤ p
i : α
hi : ¬i ∈ Set.Finite.toFinset (_ : Set.Finite {i | f i ≠ 0})
this : f i = 0
⊢ ‖f i‖ ^ ENNReal.toReal p = 0
simp [this, Real.zero_rpow hp.ne']
no goals
α : Type u_1
E : α → Type u_2
p✝ q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < ENNReal.toReal p
hfq : Memℓp f 0
hpq : 0 ≤ p
i : α
hi : ¬i ∈ Set.Finite.toFinset (_ : Set.Finite {i | f i ≠ 0})
⊢ f i = 0
simpa using hi
no goals
case inr.inr.inr.inl.intro
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f ⊤
hpq : ⊤ ≤ ⊤
⊢ Memℓp f ⊤
exact hfq
case inr.inr.inr.inr.inl.intro.hf
α : Type u_1
E : α → Type u_2
p q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < ENNReal.toReal q
hpq : q ≤ ⊤
⊢ BddAbove (Set.range fun i => ‖f i‖)
case inr.inr.inr.inr.inl.intro
α : Type u_1
E : α → Type u_2
p q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < ENNReal.toReal q
hpq : q ≤ ⊤
⊢ Memℓp f ⊤
apply memℓp_infty
case inr.inr.inr.inr.inl.intro.hf.intro
α : Type u_1
E : α → Type u_2
p q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < ENNReal.toReal q
hpq : q ≤ ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖ ^ ENNReal.toReal q)
⊢ BddAbove (Set.range fun i => ‖f i‖)
case inr.inr.inr.inr.inl.intro.hf
α : Type u_1
E : α → Type u_2
p q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < ENNReal.toReal q
hpq : q ≤ ⊤
⊢ BddAbove (Set.range fun i => ‖f i‖)
obtain ⟨A, hA⟩ := (hfq.summable hq).tendsto_cofinite_zero.bddAbove_range_of_cofinite
case inr.inr.inr.inr.inl.intro.hf.intro
α : Type u_1
E : α → Type u_2
p q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < ENNReal.toReal q
hpq : q ≤ ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖ ^ ENNReal.toReal q)
⊢ A ^ (ENNReal.toReal q)⁻¹ ∈ upperBounds (Set.range fun i => ‖f i‖)
case inr.inr.inr.inr.inl.intro.hf.intro
α : Type u_1
E : α → Type u_2
p q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < ENNReal.toReal q
hpq : q ≤ ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖ ^ ENNReal.toReal q)
⊢ BddAbove (Set.range fun i => ‖f i‖)
use A ^ q.toReal⁻¹
case inr.inr.inr.inr.inl.intro.hf.intro.intro
α : Type u_1
E : α → Type u_2
p q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < ENNReal.toReal q
hpq : q ≤ ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖ ^ ENNReal.toReal q)
i : α
⊢ (fun i => ‖f i‖) i ≤ A ^ (ENNReal.toReal q)⁻¹
case inr.inr.inr.inr.inl.intro.hf.intro
α : Type u_1
E : α → Type u_2
p q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < ENNReal.toReal q
hpq : q ≤ ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖ ^ ENNReal.toReal q)
⊢ A ^ (ENNReal.toReal q)⁻¹ ∈ upperBounds (Set.range fun i => ‖f i‖)
rintro x ⟨i, rfl⟩
case inr.inr.inr.inr.inl.intro.hf.intro.intro
α : Type u_1
E : α → Type u_2
p q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < ENNReal.toReal q
hpq : q ≤ ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖ ^ ENNReal.toReal q)
i : α
this : 0 ≤ ‖f i‖ ^ ENNReal.toReal q
⊢ (fun i => ‖f i‖) i ≤ A ^ (ENNReal.toReal q)⁻¹
case inr.inr.inr.inr.inl.intro.hf.intro.intro
α : Type u_1
E : α → Type u_2
p q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < ENNReal.toReal q
hpq : q ≤ ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖ ^ ENNReal.toReal q)
i : α
⊢ (fun i => ‖f i‖) i ≤ A ^ (ENNReal.toReal q)⁻¹
have : 0 ≤ ‖f i‖ ^ q.toReal := Real.rpow_nonneg_of_nonneg (norm_nonneg _) _
no goals
case inr.inr.inr.inr.inl.intro.hf.intro.intro
α : Type u_1
E : α → Type u_2
p q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < ENNReal.toReal q
hpq : q ≤ ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖ ^ ENNReal.toReal q)
i : α
this : 0 ≤ ‖f i‖ ^ ENNReal.toReal q
⊢ (fun i => ‖f i‖) i ≤ A ^ (ENNReal.toReal q)⁻¹
simpa [← Real.rpow_mul, mul_inv_cancel hq.ne'] using
  Real.rpow_le_rpow this (hA ⟨i, rfl⟩) (inv_nonneg.mpr hq.le)
case inr.inr.inr.inr.inr.intro.intro.hf
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
⊢ Summable fun i => ‖f i‖ ^ ENNReal.toReal p
case inr.inr.inr.inr.inr.intro.intro
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
⊢ Memℓp f p
apply memℓp_gen
case inr.inr.inr.inr.inr.intro.intro.hf
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
hf' : Summable fun i => ‖f i‖ ^ ENNReal.toReal q
⊢ Summable fun i => ‖f i‖ ^ ENNReal.toReal p
case inr.inr.inr.inr.inr.intro.intro.hf
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
⊢ Summable fun i => ‖f i‖ ^ ENNReal.toReal p
have hf' := hfq.summable hq
case inr.inr.inr.inr.inr.intro.intro.hf.refine'_1
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
hf' : Summable fun i => ‖f i‖ ^ ENNReal.toReal q
⊢ Set.Finite {i | 1 ≤ ‖f i‖}

case inr.inr.inr.inr.inr.intro.intro.hf.refine'_2
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
hf' : Summable fun i => ‖f i‖ ^ ENNReal.toReal q
⊢ {x | (fun i => ‖‖f i‖ ^ ENNReal.toReal p‖ ≤ ‖f i‖ ^ ENNReal.toReal q) x}ᶜ ⊆ {i | 1 ≤ ‖f i‖}
case inr.inr.inr.inr.inr.intro.intro.hf
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
hf' : Summable fun i => ‖f i‖ ^ ENNReal.toReal q
⊢ Summable fun i => ‖f i‖ ^ ENNReal.toReal p
refine' summable_of_norm_bounded_eventually _ hf' (@Set.Finite.subset _ { i | 1 ≤ ‖f i‖ } _ _ _)
case inr.inr.inr.inr.inr.intro.intro.hf.refine'_1
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
hf' : Summable fun i => ‖f i‖ ^ ENNReal.toReal q
H : Set.Finite {x | 1 ≤ ‖f x‖ ^ ENNReal.toReal q}
⊢ Set.Finite {i | 1 ≤ ‖f i‖}
case inr.inr.inr.inr.inr.intro.intro.hf.refine'_1
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
hf' : Summable fun i => ‖f i‖ ^ ENNReal.toReal q
⊢ Set.Finite {i | 1 ≤ ‖f i‖}
have H : { x : α | 1 ≤ ‖f x‖ ^ q.toReal }.Finite := by
  simpa using eventually_lt_of_tendsto_lt (by norm_num) hf'.tendsto_cofinite_zero
no goals
case inr.inr.inr.inr.inr.intro.intro.hf.refine'_1
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
hf' : Summable fun i => ‖f i‖ ^ ENNReal.toReal q
H : Set.Finite {x | 1 ≤ ‖f x‖ ^ ENNReal.toReal q}
⊢ Set.Finite {i | 1 ≤ ‖f i‖}
exact H.subset fun i hi => Real.one_le_rpow hi hq.le
no goals
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
hf' : Summable fun i => ‖f i‖ ^ ENNReal.toReal q
⊢ Set.Finite {x | 1 ≤ ‖f x‖ ^ ENNReal.toReal q}
simpa using eventually_lt_of_tendsto_lt (by norm_num) hf'.tendsto_cofinite_zero
no goals
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
hf' : Summable fun i => ‖f i‖ ^ ENNReal.toReal q
⊢ 0 < 1
norm_num
case inr.inr.inr.inr.inr.intro.intro.hf.refine'_2
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
hf' : Summable fun i => ‖f i‖ ^ ENNReal.toReal q
⊢ ∀ (i : α), ¬abs (‖f i‖ ^ ENNReal.toReal p) ≤ ‖f i‖ ^ ENNReal.toReal q → 1 ≤ ‖f i‖
case inr.inr.inr.inr.inr.intro.intro.hf.refine'_2
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
hf' : Summable fun i => ‖f i‖ ^ ENNReal.toReal q
⊢ {x | (fun i => ‖‖f i‖ ^ ENNReal.toReal p‖ ≤ ‖f i‖ ^ ENNReal.toReal q) x}ᶜ ⊆ {i | 1 ≤ ‖f i‖}
show ∀ i, ¬|‖f i‖ ^ p.toReal| ≤ ‖f i‖ ^ q.toReal → 1 ≤ ‖f i‖
case inr.inr.inr.inr.inr.intro.intro.hf.refine'_2
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
hf' : Summable fun i => ‖f i‖ ^ ENNReal.toReal q
i : α
hi : ¬abs (‖f i‖ ^ ENNReal.toReal p) ≤ ‖f i‖ ^ ENNReal.toReal q
⊢ 1 ≤ ‖f i‖
case inr.inr.inr.inr.inr.intro.intro.hf.refine'_2
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
hf' : Summable fun i => ‖f i‖ ^ ENNReal.toReal q
⊢ ∀ (i : α), ¬abs (‖f i‖ ^ ENNReal.toReal p) ≤ ‖f i‖ ^ ENNReal.toReal q → 1 ≤ ‖f i‖
intro i hi
case inr.inr.inr.inr.inr.intro.intro.hf.refine'_2
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
hf' : Summable fun i => ‖f i‖ ^ ENNReal.toReal q
i : α
hi : ¬abs (‖f i‖ ^ ENNReal.toReal p) ≤ ‖f i‖ ^ ENNReal.toReal q
this : 0 ≤ ‖f i‖ ^ ENNReal.toReal p
⊢ 1 ≤ ‖f i‖
case inr.inr.inr.inr.inr.intro.intro.hf.refine'_2
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
hf' : Summable fun i => ‖f i‖ ^ ENNReal.toReal q
i : α
hi : ¬abs (‖f i‖ ^ ENNReal.toReal p) ≤ ‖f i‖ ^ ENNReal.toReal q
⊢ 1 ≤ ‖f i‖
have : 0 ≤ ‖f i‖ ^ p.toReal := Real.rpow_nonneg_of_nonneg (norm_nonneg _) p.toReal
case inr.inr.inr.inr.inr.intro.intro.hf.refine'_2
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
hf' : Summable fun i => ‖f i‖ ^ ENNReal.toReal q
i : α
this : 0 ≤ ‖f i‖ ^ ENNReal.toReal p
hi : ¬‖f i‖ ^ ENNReal.toReal p ≤ ‖f i‖ ^ ENNReal.toReal q
⊢ 1 ≤ ‖f i‖
case inr.inr.inr.inr.inr.intro.intro.hf.refine'_2
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
hf' : Summable fun i => ‖f i‖ ^ ENNReal.toReal q
i : α
hi : ¬abs (‖f i‖ ^ ENNReal.toReal p) ≤ ‖f i‖ ^ ENNReal.toReal q
this : 0 ≤ ‖f i‖ ^ ENNReal.toReal p
⊢ 1 ≤ ‖f i‖
simp only [abs_of_nonneg, this] at hi
case inr.inr.inr.inr.inr.intro.intro.hf.refine'_2
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
hf' : Summable fun i => ‖f i‖ ^ ENNReal.toReal q
i : α
this : 0 ≤ ‖f i‖ ^ ENNReal.toReal p
hi : ¬1 ≤ ‖f i‖
⊢ ‖f i‖ ^ ENNReal.toReal p ≤ ‖f i‖ ^ ENNReal.toReal q
case inr.inr.inr.inr.inr.intro.intro.hf.refine'_2
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
hf' : Summable fun i => ‖f i‖ ^ ENNReal.toReal q
i : α
this : 0 ≤ ‖f i‖ ^ ENNReal.toReal p
hi : ¬‖f i‖ ^ ENNReal.toReal p ≤ ‖f i‖ ^ ENNReal.toReal q
⊢ 1 ≤ ‖f i‖
contrapose! hi
case inr.inr.inr.inr.inr.intro.intro.hf.refine'_2
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
hf' : Summable fun i => ‖f i‖ ^ ENNReal.toReal q
i : α
this : 0 ≤ ‖f i‖ ^ ENNReal.toReal p
hi : ‖f i‖ < 1
⊢ ‖f i‖ ^ ENNReal.toReal p ≤ ‖f i‖ ^ ENNReal.toReal q
case inr.inr.inr.inr.inr.intro.intro.hf.refine'_2
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
hf' : Summable fun i => ‖f i‖ ^ ENNReal.toReal q
i : α
this : 0 ≤ ‖f i‖ ^ ENNReal.toReal p
hi : ¬1 ≤ ‖f i‖
⊢ ‖f i‖ ^ ENNReal.toReal p ≤ ‖f i‖ ^ ENNReal.toReal q
rw [not_le] at hi
no goals
case inr.inr.inr.inr.inr.intro.intro.hf.refine'_2
α : Type u_1
E : α → Type u_2
p✝ q✝ : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < ENNReal.toReal q
left✝ : 0 < ENNReal.toReal p
hpq' : ENNReal.toReal q ≤ ENNReal.toReal p
hf' : Summable fun i => ‖f i‖ ^ ENNReal.toReal q
i : α
this : 0 ≤ ‖f i‖ ^ ENNReal.toReal p
hi : ‖f i‖ < 1
⊢ ‖f i‖ ^ ENNReal.toReal p ≤ ‖f i‖ ^ ENNReal.toReal q
exact Real.rpow_le_rpow_of_exponent_ge' (norm_nonneg _) hi.le hq.le hpq'