-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem norm_nonneg' (f : lp E p) : 0 ≤ ‖f‖

Proof state:
case inr.inl.inr
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
_i : Nonempty α
⊢ 0 ≤ ‖f‖

Tactic:
inhabit α

Result:
case inr.inl.inr
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
_i : Nonempty α
inhabited_h : Inhabited α
⊢ 0 ≤ ‖f‖

Proof state:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
hp : 0 < p.toReal
⊢ ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal

Tactic:
exact fun i => Real.rpow_nonneg (norm_nonneg _) _

Result:
no goals

Proof state:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
hp : 0 < p.toReal
⊢ 0 ≤ ‖f‖

Tactic:
rw [lp.norm_eq_tsum_rpow hp f]

Result:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
hp : 0 < p.toReal
⊢ 0 ≤ (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
⊢ 0 ≤ ‖f‖

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

Result:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E 0)
⊢ 0 ≤ ‖f‖

case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
⊢ 0 ≤ ‖f‖

case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
hp : 0 < p.toReal
⊢ 0 ≤ ‖f‖

Proof state:
case inr.inl.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
_i : IsEmpty α
⊢ 0 ≤ ⨆ i, ‖↑f i‖

Tactic:
simp [Real.iSup_of_isEmpty]

Result:
no goals

Proof state:
case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
⊢ 0 ≤ ‖f‖

Tactic:
rcases isEmpty_or_nonempty α with _i | _i

Result:
case inr.inl.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
_i : IsEmpty α
⊢ 0 ≤ ‖f‖

case inr.inl.inr
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
_i : Nonempty α
⊢ 0 ≤ ‖f‖

Proof state:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
hp : 0 < p.toReal
⊢ 0 ≤ (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)

Tactic:
refine Real.rpow_nonneg (tsum_nonneg ?_) _

Result:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
hp : 0 < p.toReal
⊢ ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal

Proof state:
case inr.inl.inr
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
_i : Nonempty α
inhabited_h : Inhabited α
⊢ 0 ≤ ‖f‖

Tactic:
exact (norm_nonneg (f default)).trans ((lp.isLUB_norm f).1 ⟨default, rfl⟩)

Result:
no goals

Proof state:
case inr.inl.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
_i : IsEmpty α
⊢ 0 ≤ ‖f‖

Tactic:
rw [lp.norm_eq_ciSup]

Result:
case inr.inl.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
_i : IsEmpty α
⊢ 0 ≤ ⨆ i, ‖↑f i‖

Proof state:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E 0)
⊢ 0 ≤ ‖f‖

Tactic:
simp [lp.norm_eq_card_dsupport f]

Result:
no goals