`BookProof.QgMultiHalfDensity.multiHalfDensityUnitary_apply` (g : Lp ℂ 2 (BookProof.ScalaronDensitized.physMeasure.prod mu)) : (multiHalfDensityUnitary mu g : ℝ × X → ℂ) =ᵐ[qgSrcMe

Initializing...

`BookProof.QgMultiHalfDensity.multiHalfDensityUnitary_apply` (g : Lp ℂ 2 (BookProof.ScalaronDensitized.physMeasure.prod mu)) : (multiHalfDensityUnitary mu g : ℝ × X → ℂ) =ᵐ[qgSrcMe · Prove2Me