Theorems · Theorem · measure theory

MeasureTheory.measure_lintegral_sub_measure

∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] {s : Set G} [MeasurableNeg G]
  (μ' ν' : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ'] [MeasureTheory.SigmaFinite ν']
  [μ'.IsAddLeftInvariant] [ν'.IsAddLeftInvariant],
  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) + ν(s - x) = f(x) holds if we can prove that 0 < ν(s - x) < ∞. 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_add_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

MeasurableSpaceAddGroupMeasurableAdd₂MeasurableNegMeasureTheory.SigmaFiniteMeasureTheory.SigmaFiniteMeasureTheory.Measure.IsAddLeftInvariantMeasureTheory.Measure.IsAddLeftInvariant