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

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

case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
⊢ 0 ≤ ‖f‖
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E p }
⊢ 0 ≤ ‖f‖
rcases p.trichotomy with (rfl | rfl | hp)
no goals
case inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E 0 }
⊢ 0 ≤ ‖f‖
simp [lp.norm_eq_card_dsupport f]
case inr.inl.inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E ⊤ }
_i : IsEmpty α
⊢ 0 ≤ ‖f‖

case inr.inl.inr
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E ⊤ }
_i : Nonempty α
⊢ 0 ≤ ‖f‖
case inr.inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E ⊤ }
⊢ 0 ≤ ‖f‖
cases' isEmpty_or_nonempty α with _i _i
case inr.inl.inr
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E ⊤ }
_i : Nonempty α
inhabited_h : Inhabited α
⊢ 0 ≤ ‖f‖
case inr.inl.inr
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E ⊤ }
_i : Nonempty α
⊢ 0 ≤ ‖f‖
inhabit α
no goals
case inr.inl.inr
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E ⊤ }
_i : Nonempty α
inhabited_h : Inhabited α
⊢ 0 ≤ ‖f‖
exact (norm_nonneg (f default)).trans ((lp.isLUB_norm f).1 ⟨default, rfl⟩)
case inr.inl.inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E ⊤ }
_i : IsEmpty α
⊢ 0 ≤ ⨆ (i : α), ‖↑f i‖
case inr.inl.inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E ⊤ }
_i : IsEmpty α
⊢ 0 ≤ ‖f‖
rw [lp.norm_eq_ciSup]
no goals
case inr.inl.inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E ⊤ }
_i : IsEmpty α
⊢ 0 ≤ ⨆ (i : α), ‖↑f i‖
simp [Real.ciSup_empty]
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
⊢ 0 ≤ (∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
⊢ 0 ≤ ‖f‖
rw [lp.norm_eq_tsum_rpow hp f]
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
⊢ ∀ (i : α), 0 ≤ ‖↑f i‖ ^ ENNReal.toReal p
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
⊢ 0 ≤ (∑' (i : α), ‖↑f i‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
refine' Real.rpow_nonneg_of_nonneg (tsum_nonneg _) _
no goals
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
⊢ ∀ (i : α), 0 ≤ ‖↑f i‖ ^ ENNReal.toReal p
exact fun i => Real.rpow_nonneg_of_nonneg (norm_nonneg _) _