Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.eLpNorm_two_eq_enorm_integral_mul_conj

Carleson.ToMathlib.Misc · Carleson/ToMathlib/Misc.lean:319 to 328

Source documentation

One of the very few cases where a norm can be moved out of an integral.

Exact Lean statement

lemma eLpNorm_two_eq_enorm_integral_mul_conj {f : α → ℂ} (lpf : MemLp f 2 μ) :
    eLpNorm f 2 μ ^ 2 = ‖∫ x, f x * conj (f x) ∂μ‖ₑ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma eLpNorm_two_eq_enorm_integral_mul_conj {f : α → ℂ} (lpf : MemLp f 2 μ) :    eLpNorm f 2 μ ^ 2 = ‖∫ x, f x * conj (f x) ∂μ‖ₑ := by  conv_rhs => enter [1, 2, x]; rw [RCLike.mul_conj, ← RCLike.ofReal_pow]  erw [integral_ofReal]  rw [integral_eq_lintegral_of_nonneg_ae (.of_forall fun _ ↦ by simp)]; swap  · exact lpf.aestronglyMeasurable.norm.pow 2  conv_rhs => enter [1, 1, 1, 2, x]; rw [ENNReal.ofReal_pow (norm_nonneg _), ofReal_norm]  rw [← sq_eLpNorm_two, ← enorm_norm]  simp_rw [Complex.coe_algebraMap, Complex.norm_real, enorm_norm]  rw [toReal_pow, enorm_pow, Real.enorm_toReal lpf.eLpNorm_ne_top]