Theorems · Theorem · measure theory

MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure_of_measurableSet

∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_8 : μ'.IsMulLeftInvariant]
  {s : Set G}, MeasurableSet s → IsCompact (closure s) → μ' s = μ'.haarScalarFactor μ • μ s

Given an invariant measure then it gives the same mass to measurable sets with compact closure as any other invariant measure, up to the scalar haarScalarFactor μ' μ. Auxiliary lemma in the proof of the more general measure_isMulInvariant_eq_smul_of_isCompact_closure, which removes the measurability assumption.

Defined in

Mathlib.MeasureTheory.Measure.Haar.Unique

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceGroupIsTopologicalGroupMeasurableSpaceBorelSpaceLocallyCompactSpaceMeasureTheory.Measure.IsHaarMeasureMeasureTheory.IsFiniteMeasureOnCompactsMeasureTheory.Measure.IsMulLeftInvariant