Theorems · Theorem · measure theory

IsFundamentalDomain.AddQuotientMeasureEqMeasurePreimage_vaddAddHaarMeasure

∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G]
  [inst_3 : IsTopologicalAddGroup G] [inst_4 : BorelSpace G] [inst_5 : PolishSpace G] {Γ : AddSubgroup G}
  [inst_6 : Γ.Normal] [inst_7 : T2Space (G ⧸ Γ)] [inst_8 : SecondCountableTopology (G ⧸ Γ)] [Countable ↥Γ]
  (ν : MeasureTheory.Measure G) [ν.IsAddHaarMeasure] [ν.IsAddRightInvariant] [MeasureTheory.SigmaFinite ν]
  (K : TopologicalSpace.PositiveCompacts (G ⧸ Γ)) {𝓕 : Set G},
  MeasureTheory.IsAddFundamentalDomain (↥Γ.op) 𝓕 ν →
    ν 𝓕 ≠ ⊤ →
      MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν
        (ν (QuotientAddGroup.mk ⁻¹' ↑K ∩ 𝓕) • MeasureTheory.Measure.addHaarMeasure K)

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

0 results in Mathlib

Foundations

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

Assumes

AddGroupMeasurableSpaceTopologicalSpaceIsTopologicalAddGroupBorelSpacePolishSpaceAddSubgroup.NormalT2SpaceSecondCountableTopologyCountableMeasureTheory.Measure.IsAddHaarMeasureMeasureTheory.Measure.IsAddRightInvariantMeasureTheory.SigmaFinite