Theorems · Theorem · measure theory

MeasureTheory.AddQuotientMeasureEqMeasurePreimage.vaddInvariantMeasure_quotient

∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] (ν : MeasureTheory.Measure G) {Γ : AddSubgroup G}
  {μ : MeasureTheory.Measure (G ⧸ Γ)} [MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ]
  [inst_3 : TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G] [PolishSpace G] [T2Space (G ⧸ Γ)]
  [SecondCountableTopology (G ⧸ Γ)] [ν.IsAddLeftInvariant] [hasFun : MeasureTheory.HasAddFundamentalDomain (↥Γ.op) G ν],
  MeasureTheory.VAddInvariantMeasure G (G ⧸ Γ) μ

If μ satisfies AddQuotientMeasureEqMeasurePreimage relative to a both left- and right-invariant measure ν on G, then it is a G invariant measure on G ⧸ Γ.

Defined in

Mathlib.MeasureTheory.Measure.Haar.Quotient

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddGroupMeasurableSpaceMeasureTheory.AddQuotientMeasureEqMeasurePreimageTopologicalSpaceIsTopologicalAddGroupBorelSpacePolishSpaceT2SpaceSecondCountableTopologyMeasureTheory.Measure.IsAddLeftInvariantMeasureTheory.HasAddFundamentalDomain