Theorems · Theorem · measure theory

MeasureTheory.Measure.integral_isMulLeftInvariant_isMulRightInvariant_combo

∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] [inst_3 : MeasurableSpace G]
  [BorelSpace G] {μ ν : MeasureTheory.Measure G} [MeasureTheory.IsFiniteMeasureOnCompacts μ]
  [MeasureTheory.IsFiniteMeasureOnCompacts ν] [μ.IsMulLeftInvariant] [ν.IsMulRightInvariant] [ν.IsOpenPosMeasure]
  {f g : G → ℝ},
  Continuous f →
    HasCompactSupport f →
      Continuous g →
        HasCompactSupport g →
          0 ≤ g →
            ∀ {x₀ : G},
              g x₀ ≠ 0 → ∫ (x : G), f x ∂μ = (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ (x : G), g x ∂μ

In a group with a left invariant measure μ and a right invariant measure ν, one can express integrals with respect to μ as integrals with respect to ν up to a constant scaling factor (given in the statement as ∫ x, g x ∂μ where g is a fixed reference function) and an explicit density y ↦ 1/∫ z, g (z⁻¹ * y) ∂ν.

Defined in

Mathlib.MeasureTheory.Measure.Haar.Unique

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceGroupIsTopologicalGroupMeasurableSpaceBorelSpaceMeasureTheory.IsFiniteMeasureOnCompactsMeasureTheory.IsFiniteMeasureOnCompactsMeasureTheory.Measure.IsMulLeftInvariantMeasureTheory.Measure.IsMulRightInvariantMeasureTheory.Measure.IsOpenPosMeasure