Theorems · Theorem · measure theory

MeasureTheory.Measure.IsAddLeftInvariant.addQuotientMeasureEqMeasurePreimage_of_set

∀ {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] [Countable ↥Γ] [ν.IsAddRightInvariant] [MeasureTheory.SigmaFinite ν] [μ.IsAddLeftInvariant]
  [MeasureTheory.SigmaFinite μ] {s : Set G},
  MeasureTheory.IsAddFundamentalDomain (↥Γ.op) s ν →
    ∀ {V : Set (G ⧸ Γ)},
      MeasurableSet V →
        μ V ≠ 0 →
          μ V = ν (QuotientAddGroup.mk ⁻¹' V ∩ s) → μ V ≠ ⊤ → MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ

Assume that a measure μ is IsAddLeftInvariant, that the action of Γ on G has a measurable fundamental domain s with positive finite volume, and that there is a single measurable set V ⊆ G ⧸ Γ along which the pullback of μ and ν agree (so the scaling is right). Then μ satisfies AddQuotientMeasureEqMeasurePreimage. The main tool of the proof is the uniqueness of left invariant measures, if normalized by a single positive finite-measured set.

Defined in

Mathlib.MeasureTheory.Measure.Haar.Quotient

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddGroupMeasurableSpaceTopologicalSpaceIsTopologicalAddGroupBorelSpacePolishSpaceAddSubgroup.NormalT2SpaceSecondCountableTopologyMeasureTheory.Measure.IsAddLeftInvariantCountableMeasureTheory.Measure.IsAddRightInvariantMeasureTheory.SigmaFiniteMeasureTheory.Measure.IsAddLeftInvariantMeasureTheory.SigmaFinite