`BookProof.ChapterDiffuseUnitaryModel.memLp_top_comp_cdf` {g : ℝ → ℂ} (hg : MemLp g ⊤ (volume.restrict (Set.Icc (0 : ℝ) 1))) : MemLp (fun x => g (cdf mu x)) ⊤ mu

Initializing...

`BookProof.ChapterDiffuseUnitaryModel.memLp_top_comp_cdf` {g : ℝ → ℂ} (hg : MemLp g ⊤ (volume.restrict (Set.Icc (0 : ℝ) 1))) : MemLp (fun x => g (cdf mu x)) ⊤ mu · Prove2Me