-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem norm_neg ⦃f : lp E p⦄ : ‖-f‖ = ‖f‖

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
⊢ ‖-f‖ = ‖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)
⊢ ‖-f‖ = ‖f‖

case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
⊢ ‖-f‖ = ‖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
⊢ ‖-f‖ = ‖f‖

Proof state:
case inr.inl.inr
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
h✝ : Nonempty α
⊢ IsLUB (Set.range fun i => ‖↑(-f) i‖) ‖f‖

Tactic:
simpa only [coeFn_neg, Pi.neg_apply, norm_neg] using lp.isLUB_norm f

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
⊢ HasSum (fun i => ‖↑(-f) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)

Tactic:
simpa only [coeFn_neg, Pi.neg_apply, _root_.norm_neg] using lp.hasSum_norm hp f

Result:
no goals

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

Tactic:
exact Real.rpow_left_injOn hp.ne' (norm_nonneg' _) (norm_nonneg' _) this

Result:
no goals

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

Tactic:
cases isEmpty_or_nonempty α

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

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

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

Tactic:
simp only [lp.eq_zero' f, neg_zero, norm_zero]

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
⊢ ‖-f‖ ^ p.toReal = ‖f‖ ^ p.toReal

Tactic:
apply (lp.hasSum_norm hp (-f)).unique

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
⊢ HasSum (fun i => ‖↑(-f) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)

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

Tactic:
apply (lp.isLUB_norm (-f)).unique

Result:
case inr.inl.inr
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
h✝ : Nonempty α
⊢ IsLUB (Set.range fun i => ‖↑(-f) i‖) ‖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
⊢ ‖-f‖ = ‖f‖

Tactic:
suffices ‖-f‖ ^ p.toReal = ‖f‖ ^ p.toReal by
  exact Real.rpow_left_injOn hp.ne' (norm_nonneg' _) (norm_nonneg' _) this

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
⊢ ‖-f‖ ^ p.toReal = ‖f‖ ^ p.toReal

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

Tactic:
simp only [norm_eq_card_dsupport, coeFn_neg, Pi.neg_apply, ne_eq, neg_eq_zero]

Result:
no goals