`BookProof.QgMultiHalfDensity.mpUnitary_symm_apply` (hPhi : MeasurePreserving Phi mu nu) (hPsi : MeasurePreserving Psi nu mu) (hinv : ∀ᵐ x ∂mu, Psi (Phi x) = x) (h : Lp ℂ 2 mu) : (

Initializing...

`BookProof.QgMultiHalfDensity.mpUnitary_symm_apply` (hPhi : MeasurePreserving Phi mu nu) (hPsi : MeasurePreserving Psi nu mu) (hinv : ∀ᵐ x ∂mu, Psi (Phi x) = x) (h : Lp ℂ 2 mu) : ( · Prove2Me