`BookProof.ChapterBornMeasure.lintegral_bornDensity` (psi : Lp ℂ 2 μ) (hpsi : ‖psi‖ = 1) : ∫⁻ x, ‖(psi : α → ℂ) x‖ₑ ^ 2 ∂μ = 1

Initializing...

`BookProof.ChapterBornMeasure.lintegral_bornDensity` (psi : Lp ℂ 2 μ) (hpsi : ‖psi‖ = 1) : ∫⁻ x, ‖(psi : α → ℂ) x‖ₑ ^ 2 ∂μ = 1 · Prove2Me