English
Norm is invariant under negation: ‖-f‖ = ‖f‖.
Русский
Норма не меняется при заменe f на −f: ‖−f‖ = ‖f‖.
LaTeX
$$$$ \| -f \| = \| f \|. $$$$
Lean4
@[simp]
theorem norm_neg ⦃f : lp E p⦄ : ‖-f‖ = ‖f‖ :=
by
rcases p.trichotomy with (rfl | rfl | hp)
· simp only [norm_eq_card_dsupport, coeFn_neg, Pi.neg_apply, ne_eq, neg_eq_zero]
· cases isEmpty_or_nonempty α
· simp only [lp.eq_zero' f, neg_zero, norm_zero]
apply (lp.isLUB_norm (-f)).unique
simpa only [coeFn_neg, Pi.neg_apply, norm_neg] using lp.isLUB_norm f
· suffices ‖-f‖ ^ p.toReal = ‖f‖ ^ p.toReal by
exact Real.rpow_left_injOn hp.ne' (norm_nonneg' _) (norm_nonneg' _) this
apply (lp.hasSum_norm hp (-f)).unique
simpa only [coeFn_neg, Pi.neg_apply, _root_.norm_neg] using lp.hasSum_norm hp f
