Theorems · Theorem · measure theory

MeasureTheory.QuotientMeasureEqMeasurePreimage.haarMeasure_quotient

∀ {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] [LocallyCompactSpace G] [MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ]
  [i : MeasureTheory.HasFundamentalDomain (↥Γ.op) G ν] [MeasureTheory.IsFiniteMeasure μ], μ.IsHaarMeasure

If a measure μ on the quotient G ⧸ Γ of a group G by a discrete normal subgroup Γ having fundamental domain, satisfies QuotientMeasureEqMeasurePreimage relative to a standardized choice of Haar measure on G, and assuming μ is finite, then μ is itself Haar. TODO: Is it possible to drop the assumption that μ is finite?

Defined in

Mathlib.MeasureTheory.Measure.Haar.Quotient

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupMeasurableSpaceTopologicalSpaceIsTopologicalGroupBorelSpacePolishSpaceSubgroup.NormalT2SpaceSecondCountableTopologyCountableMeasureTheory.Measure.IsHaarMeasureMeasureTheory.Measure.IsMulRightInvariantLocallyCompactSpaceMeasureTheory.QuotientMeasureEqMeasurePreimageMeasureTheory.HasFundamentalDomainMeasureTheory.IsFiniteMeasure