Theorems · Theorem · measure theory

MeasureTheory.Measure.smul_measure_isMulInvariant_le_of_isCompact_closure

∀ {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]
  [μ.InnerRegularCompactLTTop] {s : Set G}, MeasurableSet s → IsCompact (closure s) → μ'.haarScalarFactor μ • μ s ≤ μ' s

If an invariant measure is inner regular, then it gives less mass to sets with compact closure than 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 gives equality for any set with compact closure.

Defined in

Mathlib.MeasureTheory.Measure.Haar.Unique

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceGroupIsTopologicalGroupMeasurableSpaceBorelSpaceLocallyCompactSpaceMeasureTheory.Measure.IsHaarMeasureMeasureTheory.IsFiniteMeasureOnCompactsMeasureTheory.Measure.IsMulLeftInvariantMeasureTheory.Measure.InnerRegularCompactLTTop