Theorems · Theorem · measure theory

MeasureTheory.measure_lintegral_div_measure

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

A technical lemma relating two different measures. This is basically [Halmos, §60 Th. A]. Note that if f is the characteristic function of a measurable set t this states that μ t = c * μ s for a constant c that does not depend on μ. Note: There is a gap in the last step of the proof in [Halmos]. In the last line, the equality g(x⁻¹)ν(sx⁻¹) = f(x) holds if we can prove that 0 < ν(sx⁻¹) < ∞. The first inequality follows from §59, Th. D, but the second inequality is not justified. We prove this inequality for almost all x in MeasureTheory.ae_measure_preimage_mul_right_lt_top_of_ne_zero.

Defined in

Mathlib.MeasureTheory.Group.Prod

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceGroupMeasurableMul₂MeasurableInvMeasureTheory.SigmaFiniteMeasureTheory.SigmaFiniteMeasureTheory.Measure.IsMulLeftInvariantMeasureTheory.Measure.IsMulLeftInvariant