Prove2Me

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

Proved
BookProof.ChapterPvmScalarMeasure.exists_quasiInvariant_scalarMeasure

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterPvmScalarMeasure.

BookProof.ChapterPvmScalarMeasure.exists_quasiInvariant_scalarMeasure [CompleteSpace H] [TopologicalSpace.SeparableSpace H] (T : ContinuousImprimitivitySystem G X H) : ∃ μ : Measure X, IsFiniteMeasure μ ∧ QuasiInvariant μ G ∧ ∀ E : Set X, MeasurableSet E → (μ E = 0 ↔ T.P.p E = 0)

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

Preamble
-- Generated from ChapterPvmScalarMeasure.lean — theorem BookProof.ChapterPvmScalarMeasure.exists_quasiInvariant_scalarMeasure
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_ChapterMackeyQuasiInvariant
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_quasiInvariant_scalarMeasure [CompleteSpace H]
    [TopologicalSpace.SeparableSpace H] (T : ContinuousImprimitivitySystem G X H) :
    ∃ μ : Measure X, IsFiniteMeasure μ ∧ QuasiInvariant μ G ∧
      ∀ E : Set X, MeasurableSet E → (μ E = 0 ↔ T.P.p E = 0) := by sorry

View graph