Theorems · Theorem · measure theory

MeasureTheory.Measure.measure_preimage_isAddLeftInvariant_eq_smul_of_hasCompactSupport

∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ' μ : MeasureTheory.Measure G) [inst_5 : μ.IsAddHaarMeasure]
  [inst_6 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_7 : μ'.IsAddLeftInvariant] {f : G → ℝ},
  Continuous f → HasCompactSupport f → μ' (f ⁻¹' {1}) = μ'.addHaarScalarFactor μ • μ (f ⁻¹' {1})

Two left invariant measures give the same mass to level sets of continuous compactly supported functions, up to the scalar addHaarScalarFactor μ' μ. Auxiliary lemma in the proof of the more general measure_isAddInvariant_eq_smul_of_isCompact_closure, which works for any set with compact closure.

Defined in

Mathlib.MeasureTheory.Measure.Haar.Unique

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddGroupIsTopologicalAddGroupMeasurableSpaceBorelSpaceMeasureTheory.Measure.IsAddHaarMeasureMeasureTheory.IsFiniteMeasureOnCompactsMeasureTheory.Measure.IsAddLeftInvariant