case inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
i : α
hp : ⊤ ≠ 0
f : { x // x ∈ lp E ⊤ }
⊢ ‖↑f i‖ ≤ ‖f‖

case inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : { x // x ∈ lp E p }
i : α
hp' : p ≠ ⊤
⊢ ‖↑f i‖ ≤ ‖f‖
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : { x // x ∈ lp E p }
i : α
⊢ ‖↑f i‖ ≤ ‖f‖
rcases eq_or_ne p ∞ with (rfl | hp')
case inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : { x // x ∈ lp E p }
i : α
hp' : p ≠ ⊤
hp'' : 0 < ENNReal.toReal p
⊢ ‖↑f i‖ ≤ ‖f‖
case inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : { x // x ∈ lp E p }
i : α
hp' : p ≠ ⊤
⊢ ‖↑f i‖ ≤ ‖f‖
have hp'' : 0 < p.toReal := ENNReal.toReal_pos hp hp'
case inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : { x // x ∈ lp E p }
i : α
hp' : p ≠ ⊤
hp'' : 0 < ENNReal.toReal p
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ ENNReal.toReal p
⊢ ‖↑f i‖ ≤ ‖f‖
case inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : { x // x ∈ lp E p }
i : α
hp' : p ≠ ⊤
hp'' : 0 < ENNReal.toReal p
⊢ ‖↑f i‖ ≤ ‖f‖
have : ∀ i, 0 ≤ ‖f i‖ ^ p.toReal := fun i => Real.rpow_nonneg_of_nonneg (norm_nonneg _) _
case inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : { x // x ∈ lp E p }
i : α
hp' : p ≠ ⊤
hp'' : 0 < ENNReal.toReal p
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ ENNReal.toReal p
⊢ ‖↑f i‖ ^ ENNReal.toReal p ≤ ‖f‖ ^ ENNReal.toReal p
case inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : { x // x ∈ lp E p }
i : α
hp' : p ≠ ⊤
hp'' : 0 < ENNReal.toReal p
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ ENNReal.toReal p
⊢ ‖↑f i‖ ≤ ‖f‖
rw [← Real.rpow_le_rpow_iff (norm_nonneg _) (norm_nonneg' _) hp'']
no goals
case inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : { x // x ∈ lp E p }
i : α
hp' : p ≠ ⊤
hp'' : 0 < ENNReal.toReal p
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ ENNReal.toReal p
⊢ ‖↑f i‖ ^ ENNReal.toReal p ≤ ‖f‖ ^ ENNReal.toReal p
convert le_hasSum (hasSum_norm hp'' f) i fun i _ => this i
case inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
i : α
hp : ⊤ ≠ 0
f : { x // x ∈ lp E ⊤ }
this : Nonempty α
⊢ ‖↑f i‖ ≤ ‖f‖
case inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
i : α
hp : ⊤ ≠ 0
f : { x // x ∈ lp E ⊤ }
⊢ ‖↑f i‖ ≤ ‖f‖
haveI : Nonempty α := ⟨i⟩
no goals
case inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
i : α
hp : ⊤ ≠ 0
f : { x // x ∈ lp E ⊤ }
this : Nonempty α
⊢ ‖↑f i‖ ≤ ‖f‖
exact (isLUB_norm f).1 ⟨i, rfl⟩