Prove2Me

`BookProof.ChapterDiffuseUnitaryModel.cdfUnitary_apply` (f : Lp ℂ 2 (volume.restrict (Set.Icc (0 : ℝ) 1))) : cdfUnitary mu f = cdfComp mu f

Proved
BookProof.ChapterDiffuseUnitaryModel.cdfUnitary_apply

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterDiffuseUnitaryModel.

BookProof.ChapterDiffuseUnitaryModel.cdfUnitary_apply (f : Lp ℂ 2 (volume.restrict (Set.Icc (0 : ℝ) 1))) : cdfUnitary mu f = cdfComp mu f

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

Preamble
-- Generated from ChapterDiffuseUnitaryModel.lean — theorem BookProof.ChapterDiffuseUnitaryModel.cdfUnitary_apply
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.cdfUnitary_apply (f : Lp ℂ 2 (volume.restrict (Set.Icc (0 : ℝ) 1))) :
    cdfUnitary mu f = cdfComp mu f := by sorry

View graph