`BookProof.ChapterDiffuseUnitaryModel.cdfUnitary_intertwines` {g : ℝ → ℂ} (hg : MemLp g ⊤ (volume.restrict (Set.Icc (0 : ℝ) 1))) (u : Lp ℂ 2 (volume.restrict (Set.Icc (0 : ℝ) 1)))

Initializing...

`BookProof.ChapterDiffuseUnitaryModel.cdfUnitary_intertwines` {g : ℝ → ℂ} (hg : MemLp g ⊤ (volume.restrict (Set.Icc (0 : ℝ) 1))) (u : Lp ℂ 2 (volume.restrict (Set.Icc (0 : ℝ) 1))) · Prove2Me