Theorems · Theorem · measure theory

MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addInvariantMeasure_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 ⧸ Γ)} (ν : MeasureTheory.Measure G)
  [ν.IsAddLeftInvariant] [hasFun : MeasureTheory.HasAddFundamentalDomain (↥Γ.op) G ν]
  [MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ], μ.IsAddLeftInvariant

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

Defined in

Mathlib.MeasureTheory.Measure.Haar.Quotient

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddGroupMeasurableSpaceTopologicalSpaceIsTopologicalAddGroupBorelSpacePolishSpaceAddSubgroup.NormalT2SpaceSecondCountableTopologyMeasureTheory.Measure.IsAddLeftInvariantMeasureTheory.HasAddFundamentalDomainMeasureTheory.AddQuotientMeasureEqMeasurePreimage