Theorems · Theorem · measure theory

IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_HaarMeasure

∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G] [IsTopologicalGroup G]
  [BorelSpace G] [PolishSpace G] {Γ : Subgroup G} [inst_6 : Γ.Normal] [T2Space (G ⧸ Γ)]
  [SecondCountableTopology (G ⧸ Γ)] {μ : MeasureTheory.Measure (G ⧸ Γ)} [Countable ↥Γ] (ν : MeasureTheory.Measure G)
  [ν.IsHaarMeasure] [ν.IsMulRightInvariant] [MeasureTheory.SigmaFinite ν] {𝓕 : Set G},
  MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 ν →
    ∀ [μ.IsMulLeftInvariant] [MeasureTheory.SigmaFinite μ] {V : Set (G ⧸ Γ)},
      (interior V).Nonempty →
        MeasurableSet V →
          μ V = ν (QuotientGroup.mk ⁻¹' V ∩ 𝓕) → μ V ≠ ⊤ → MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ

Given a normal subgroup Γ of a topological group G with Haar measure μ, which is also right-invariant, and a finite volume fundamental domain 𝓕, the quotient map to G ⧸ Γ, properly normalized, satisfies QuotientMeasureEqMeasurePreimage.

Defined in

Mathlib.MeasureTheory.Measure.Haar.Quotient

Cited by

1 results in Mathlib

Foundations

Depth 235 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupMeasurableSpaceTopologicalSpaceIsTopologicalGroupBorelSpacePolishSpaceSubgroup.NormalT2SpaceSecondCountableTopologyCountableMeasureTheory.Measure.IsHaarMeasureMeasureTheory.Measure.IsMulRightInvariantMeasureTheory.SigmaFiniteMeasureTheory.Measure.IsMulLeftInvariantMeasureTheory.SigmaFinite