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

Proved

BookProof.ChapterDiffuseUnitaryModel.memLp_top_comp_cdf

by leonardopedro · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterDiffuseUnitaryModel.

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

Formalization note: Lean 4 identifier BookProof.ChapterDiffuseUnitaryModel.memLp_top_comp_cdf.

Preamble

-- Generated from ChapterDiffuseUnitaryModel.lean — theorem BookProof.ChapterDiffuseUnitaryModel.memLp_top_comp_cdf
import Definitions.Def_ChapterDiffuseCdfModel
import Definitions.Def_ChapterLinftyMultiplication
import Mathlib
import Definitions.Def_ChapterDiffuseUnitaryModel
open BookProof.ChapterDiffuseUnitaryModel


noncomputable section

open MeasureTheory ProbabilityTheory Filter


open BookProof.ChapterDiffuseCdfModel BookProof.ChapterLinftyMultiplication

variable (mu : Measure ℝ) [IsProbabilityMeasure mu] [NullSingletonClass mu]

Formal statement

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

View graph