`BookProof.ChapterPvmFibreInducedSystem.homEmb_apply` (hmu : ∀ ψ : S, pvmMeasure P (ψ : H) = μ) (ψ : S) (f : Lp ℂ 2 μ) : homEmb hmu ψ f = swIsom P (ψ : H) ((lpCongr (hmu ψ)).symm f

Proved

BookProof.ChapterPvmFibreInducedSystem.homEmb_apply

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterPvmFibreInducedSystem.

BookProof.ChapterPvmFibreInducedSystem.homEmb_apply (hmu : ∀ ψ : S, pvmMeasure P (ψ : H) = μ) (ψ : S) (f : Lp ℂ 2 μ) : homEmb hmu ψ f = swIsom P (ψ : H) ((lpCongr (hmu ψ)).symm f)

Formalization note: Lean 4 identifier BookProof.ChapterPvmFibreInducedSystem.homEmb_apply.

Preamble

-- Generated from ChapterPvmFibreInducedSystem.lean — theorem BookProof.ChapterPvmFibreInducedSystem.homEmb_apply
import Definitions.Def_ChapterPvmMeasure
import Definitions.Def_ChapterPvmCyclicUnitary
import Definitions.Def_ChapterPvmCyclicDecomposition
import Definitions.Def_ChapterPvmInducedSystem
import Definitions.Def_ChapterMackeyQuasiInvariant
import Definitions.Def_ChapterL2FibreSum
import Definitions.Def_ChapterHilbertSumIntertwine
import Mathlib
import Definitions.Def_ChapterPvmFibreInducedSystem
open BookProof.ChapterPvmFibreInducedSystem


open MeasureTheory
open scoped InnerProductSpace


open BookProof.ChapterPvmMeasure BookProof.ChapterPvmCyclicUnitary
open BookProof.ChapterPvmCyclicDecomposition BookProof.ChapterPvmInducedSystem
open BookProof.ChapterMackeyQuasiInvariant BookProof.ChapterL2FibreSum
open BookProof.ChapterHilbertSumIntertwine

variable {X : Type*} [MeasurableSpace X]
variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]

variable {P : Pvm X H} {S : Set H} {μ : Measure X}

Formal statement

theorem BookProof.ChapterPvmFibreInducedSystem.homEmb_apply (hmu : ∀ ψ : S, pvmMeasure P (ψ : H) = μ) (ψ : S) (f : Lp ℂ 2 μ) :
    homEmb hmu ψ f = swIsom P (ψ : H) ((lpCongr (hmu ψ)).symm f) := by sorry

View graph