Theorems · Theorem · measure theory

IsFundamentalDomain.AddQuotientMeasureEqMeasurePreimage_AddHaarMeasure

∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G]
  [IsTopologicalAddGroup G] [BorelSpace G] [PolishSpace G] {Γ : AddSubgroup G} [inst_6 : Γ.Normal] [T2Space (G ⧸ Γ)]
  [SecondCountableTopology (G ⧸ Γ)] {μ : MeasureTheory.Measure (G ⧸ Γ)} [Countable ↥Γ] (ν : MeasureTheory.Measure G)
  [ν.IsAddHaarMeasure] [ν.IsAddRightInvariant] [MeasureTheory.SigmaFinite ν] {𝓕 : Set G},
  MeasureTheory.IsAddFundamentalDomain (↥Γ.op) 𝓕 ν →
    ∀ [μ.IsAddLeftInvariant] [MeasureTheory.SigmaFinite μ] {V : Set (G ⧸ Γ)},
      (interior V).Nonempty →
        MeasurableSet V →
          μ V = ν (QuotientAddGroup.mk ⁻¹' V ∩ 𝓕) → μ V ≠ ⊤ → MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ

Given a normal subgroup Γ of an additive 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 AddQuotientMeasureEqMeasurePreimage.

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

AddGroupMeasurableSpaceTopologicalSpaceIsTopologicalAddGroupBorelSpacePolishSpaceAddSubgroup.NormalT2SpaceSecondCountableTopologyCountableMeasureTheory.Measure.IsAddHaarMeasureMeasureTheory.Measure.IsAddRightInvariantMeasureTheory.SigmaFiniteMeasureTheory.Measure.IsAddLeftInvariantMeasureTheory.SigmaFinite