Theorems · Theorem · measure theory

QuotientGroup.integral_eq_integral_automorphize

∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G] [IsTopologicalGroup G]
  [BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : Subgroup G} {𝓕 : Set G},
  MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 μ →
    ∀ [Countable ↥Γ] [inst_6 : MeasurableSpace (G ⧸ Γ)] [BorelSpace (G ⧸ Γ)] {E : Type u_2}
      [inst_8 : NormedAddCommGroup E] [inst_9 : NormedSpace ℝ E] [μ.IsMulRightInvariant] {f : G → E},
      MeasureTheory.Integrable f μ →
        MeasureTheory.AEStronglyMeasurable (QuotientGroup.automorphize f)
            (MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕)) →
          ∫ (x : G), f x ∂μ =
            ∫ (x : G ⧸ Γ), QuotientGroup.automorphize f x ∂MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕)

This is a simple version of the Unfolding Trick: Given a subgroup Γ of a group G, the integral of a function f on G with respect to a right-invariant measure μ is equal to the integral over the quotient G ⧸ Γ of the automorphization of f.

Defined in

Mathlib.MeasureTheory.Measure.Haar.Quotient

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupMeasurableSpaceTopologicalSpaceIsTopologicalGroupBorelSpaceCountableMeasurableSpaceBorelSpaceNormedAddCommGroupNormedSpaceMeasureTheory.Measure.IsMulRightInvariant