case hf
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i in s, ‖f i‖ ^ ENNReal.toReal p ≤ C
⊢ Summable fun i => ‖f i‖ ^ ENNReal.toReal p
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i in s, ‖f i‖ ^ ENNReal.toReal p ≤ C
⊢ Memℓp f p
apply memℓp_gen
case hf
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i in s, ‖f i‖ ^ ENNReal.toReal p ≤ C
⊢ HasSum (fun i => ‖f i‖ ^ ENNReal.toReal p) (⨆ (s : Finset α), ∑ i in s, ‖f i‖ ^ ENNReal.toReal p)
case hf
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i in s, ‖f i‖ ^ ENNReal.toReal p ≤ C
⊢ Summable fun i => ‖f i‖ ^ ENNReal.toReal p
use ⨆ s : Finset α, ∑ i in s, ‖f i‖ ^ p.toReal
case hf.h
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i in s, ‖f i‖ ^ ENNReal.toReal p ≤ C
⊢ ∀ (i : α), 0 ≤ ‖f i‖ ^ ENNReal.toReal p

case hf.hf
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i in s, ‖f i‖ ^ ENNReal.toReal p ≤ C
⊢ IsLUB (Set.range fun s => ∑ i in s, ‖f i‖ ^ ENNReal.toReal p) (⨆ (s : Finset α), ∑ i in s, ‖f i‖ ^ ENNReal.toReal p)
case hf
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i in s, ‖f i‖ ^ ENNReal.toReal p ≤ C
⊢ HasSum (fun i => ‖f i‖ ^ ENNReal.toReal p) (⨆ (s : Finset α), ∑ i in s, ‖f i‖ ^ ENNReal.toReal p)
apply hasSum_of_isLUB_of_nonneg
case hf.hf.H
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i in s, ‖f i‖ ^ ENNReal.toReal p ≤ C
⊢ BddAbove (Set.range fun s => ∑ i in s, ‖f i‖ ^ ENNReal.toReal p)
case hf.hf
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i in s, ‖f i‖ ^ ENNReal.toReal p ≤ C
⊢ IsLUB (Set.range fun s => ∑ i in s, ‖f i‖ ^ ENNReal.toReal p) (⨆ (s : Finset α), ∑ i in s, ‖f i‖ ^ ENNReal.toReal p)
apply isLUB_ciSup
case hf.hf.H
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i in s, ‖f i‖ ^ ENNReal.toReal p ≤ C
⊢ C ∈ upperBounds (Set.range fun s => ∑ i in s, ‖f i‖ ^ ENNReal.toReal p)
case hf.hf.H
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i in s, ‖f i‖ ^ ENNReal.toReal p ≤ C
⊢ BddAbove (Set.range fun s => ∑ i in s, ‖f i‖ ^ ENNReal.toReal p)
use C
case hf.hf.H.intro
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i in s, ‖f i‖ ^ ENNReal.toReal p ≤ C
s : Finset α
⊢ (fun s => ∑ i in s, ‖f i‖ ^ ENNReal.toReal p) s ≤ C
case hf.hf.H
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i in s, ‖f i‖ ^ ENNReal.toReal p ≤ C
⊢ C ∈ upperBounds (Set.range fun s => ∑ i in s, ‖f i‖ ^ ENNReal.toReal p)
rintro - ⟨s, rfl⟩
no goals
case hf.hf.H.intro
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i in s, ‖f i‖ ^ ENNReal.toReal p ≤ C
s : Finset α
⊢ (fun s => ∑ i in s, ‖f i‖ ^ ENNReal.toReal p) s ≤ C
exact hf s
case hf.h
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i in s, ‖f i‖ ^ ENNReal.toReal p ≤ C
b : α
⊢ 0 ≤ ‖f b‖ ^ ENNReal.toReal p
case hf.h
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i in s, ‖f i‖ ^ ENNReal.toReal p ≤ C
⊢ ∀ (i : α), 0 ≤ ‖f i‖ ^ ENNReal.toReal p
intro b
no goals
case hf.h
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i in s, ‖f i‖ ^ ENNReal.toReal p ≤ C
b : α
⊢ 0 ≤ ‖f b‖ ^ ENNReal.toReal p
exact Real.rpow_nonneg_of_nonneg (norm_nonneg _) _