`BookProof.ChapterPvmScalarMeasure.exists_induced_system_in_measure_class` [CompleteSpace H] [TopologicalSpace.SeparableSpace H] (T : ContinuousImprimitivitySystem G X H) : ∃ (μ :

Proved

BookProof.ChapterPvmScalarMeasure.exists_induced_system_in_measure_class

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterPvmScalarMeasure.

BookProof.ChapterPvmScalarMeasure.exists_induced_system_in_measure_class [CompleteSpace H] [TopologicalSpace.SeparableSpace H] (T : ContinuousImprimitivitySystem G X H) : ∃ (μ : Measure X) (S : Set H) (W : H ≃ₗᵢ[ℂ] lp (fun ψ : S => Lp ℂ 2 (pvmMeasure T.P (ψ : H))) 2), IsFiniteMeasure μ ∧ QuasiInvariant μ G ∧ S.Countable ∧ (∀ ψ ∈ S, ‖ψ‖ = 1) ∧ (∀ ψ : S, pvmMeasure T.P (ψ : H) ≪ μ) ∧ (∀ (E : Set X) (hE : MeasurableSet E) (v : H) (ψ : S), W (T.P.p E v) ψ = proj (pvmMeasure T.P (ψ : H)) hE (W v ψ))

Formalization note: Lean 4 identifier BookProof.ChapterPvmScalarMeasure.exists_induced_system_in_measure_class.

Preamble

-- Generated from ChapterPvmScalarMeasure.lean — theorem BookProof.ChapterPvmScalarMeasure.exists_induced_system_in_measure_class
import Definitions.Def_ChapterPvmMeasure
import Definitions.Def_ChapterPvmCyclicDecomposition
import Definitions.Def_ChapterMackeyConverse
import Definitions.Def_ChapterPvmInducedSystem
import Mathlib
import Definitions.Def_ChapterPvmScalarMeasure
import Definitions.Def_ChapterElectroweakFieldStrength
import Definitions.Def_ChapterMackeyQuasiInvariant
open BookProof.ChapterElectroweakFieldStrength
open BookProof.ChapterMackeyQuasiInvariant
open BookProof.ChapterPvmScalarMeasure


open MeasureTheory
open scoped InnerProductSpace


open BookProof.ChapterPvmMeasure BookProof.ChapterPvmCyclicDecomposition
open BookProof.ChapterMackeyQuasiInvariant BookProof.ChapterMackeyConverse
open BookProof.ChapterPvmInducedSystem

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

variable {G : Type*} [Group G] [MulAction G X]

Formal statement

theorem BookProof.ChapterPvmScalarMeasure.exists_induced_system_in_measure_class [CompleteSpace H]
    [TopologicalSpace.SeparableSpace H] (T : ContinuousImprimitivitySystem G X H) :
    ∃ (μ : Measure X) (S : Set H)
      (W : H ≃ₗᵢ[ℂ] lp (fun ψ : S => Lp ℂ 2 (pvmMeasure T.P (ψ : H))) 2),
      IsFiniteMeasure μ ∧ QuasiInvariant μ G ∧ S.Countable ∧
      (∀ ψ ∈ S, ‖ψ‖ = 1) ∧
      (∀ ψ : S, pvmMeasure T.P (ψ : H) ≪ μ) ∧
      (∀ (E : Set X) (hE : MeasurableSet E) (v : H) (ψ : S),
        W (T.P.p E v) ψ = proj (pvmMeasure T.P (ψ : H)) hE (W v ψ)) := by sorry

View graph