Theorems · Theorem · measure theory

MeasureTheory.leftInvariantIsQuotientMeasureEqMeasurePreimage

∀ {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 ⧸ Γ)} (ν : MeasureTheory.Measure G)
  [ν.IsMulLeftInvariant] [Countable ↥Γ] [ν.IsMulRightInvariant] [MeasureTheory.SigmaFinite ν] [μ.IsMulLeftInvariant]
  [MeasureTheory.SigmaFinite μ] [MeasureTheory.IsFiniteMeasure μ]
  [hasFun : MeasureTheory.HasFundamentalDomain (↥Γ.op) G ν],
  MeasureTheory.covolume (↥Γ.op) G ν = μ Set.univ → MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ

If a measure μ is left-invariant and satisfies the right scaling condition, then it satisfies QuotientMeasureEqMeasurePreimage.

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.NormalT2SpaceSecondCountableTopologyMeasureTheory.Measure.IsMulLeftInvariantCountableMeasureTheory.Measure.IsMulRightInvariantMeasureTheory.SigmaFiniteMeasureTheory.Measure.IsMulLeftInvariantMeasureTheory.SigmaFiniteMeasureTheory.IsFiniteMeasureMeasureTheory.HasFundamentalDomain