Theorems · Theorem · measure theory

MeasureTheory.measure_mul_lintegral_eq

∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {s : Set G} [MeasurableInv G] [μ.IsMulLeftInvariant]
  [ν.IsMulLeftInvariant],
  MeasurableSet s →
    ∀ (f : G → ENNReal), Measurable f → μ s * ∫⁻ (y : G), f y ∂ν = ∫⁻ (x : G), ν ((fun z => z * x) ⁻¹' s) * f x⁻¹ ∂μ

This is the computation performed in the proof of [Halmos, §60 Th. A].

Defined in

Mathlib.MeasureTheory.Group.Prod

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceGroupMeasurableMul₂MeasureTheory.SFiniteMeasureTheory.SFiniteMeasurableInvMeasureTheory.Measure.IsMulLeftInvariantMeasureTheory.Measure.IsMulLeftInvariant