Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.dLpNorm_conjneg

APAP.Prereqs.LpNorm.Discrete.Basic · APAP/Prereqs/LpNorm/Discrete/Basic.lean:100 to 110

Mathematical statement

Exact Lean statement

@[simp] lemma dLpNorm_conjneg [RCLike E] (f : G → E) : ‖conjneg f‖_[p] = ‖f‖_[p]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[simp] lemma dLpNorm_conjneg [RCLike E] (f : G → E) : ‖conjneg f‖_[p] = ‖f‖_[p] := by  cases nonempty_fintype G  simp only [conjneg, dLpNorm_conj]  obtain p | p := p  · simp only [dLinftyNorm_eq_iSup_norm, ENNReal.none_eq_top]    exact (Equiv.neg _).iSup_congr fun _ ↦ rfl  obtain rfl | hp := eq_or_ne p 0  · simp only [dLpNorm_exponent_zero, ENNReal.some_eq_coe, ENNReal.coe_zero]  · simp only [dLpNorm_eq_sum_norm hp, ENNReal.some_eq_coe]    congr 1    exact Fintype.sum_equiv (Equiv.neg _) _ _ fun _ ↦ rfl