Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.cLpNorm_conjneg

APAP.Prereqs.LpNorm.Compact · APAP/Prereqs/LpNorm/Compact.lean:398 to 408

Mathematical statement

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[simp] lemma cLpNorm_conjneg [RCLike E] (f : G → E) : ‖conjneg f‖ₙ_[p] = ‖f‖ₙ_[p] := by  cases nonempty_fintype G  simp only [conjneg, cLpNorm_conj]  obtain p | p := p  · simp only [cLpNorm_exponent_top_eq_essSup, ENNReal.none_eq_top]    exact (Equiv.neg _).iSup_congr fun _ ↦ rfl  obtain rfl | hp := eq_or_ne p 0  · simp only [cLpNorm_exponent_zero, ENNReal.some_eq_coe, ENNReal.coe_zero]  · simp only [cLpNorm_eq_expect_norm hp, ENNReal.some_eq_coe]    congr 1    exact Fintype.expect_equiv (Equiv.neg _) _ _ fun _ ↦ rfl