Theorems · Theorem · measure theory

MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addHaarMeasure_quotient

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

If a measure μ on the quotient G ⧸ Γ of an additive group G by a discrete normal subgroup Γ having fundamental domain, satisfies AddQuotientMeasureEqMeasurePreimage relative to a standardized choice of Haar measure on G, and assuming μ is finite, then μ is itself Haar.

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

AddGroupMeasurableSpaceTopologicalSpaceIsTopologicalAddGroupBorelSpacePolishSpaceAddSubgroup.NormalT2SpaceSecondCountableTopologyCountableMeasureTheory.Measure.IsAddHaarMeasureMeasureTheory.Measure.IsAddRightInvariantLocallyCompactSpaceMeasureTheory.AddQuotientMeasureEqMeasurePreimageMeasureTheory.HasAddFundamentalDomainMeasureTheory.IsFiniteMeasure