Theorems · Theorem · measure theory

MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop

∀ {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) → μ' s = μ'.haarScalarFactor μ • μ s

If an invariant measure is inner regular, 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 works for any set with compact closure, and removes the inner regularity assumption.

Defined in

Mathlib.MeasureTheory.Measure.Haar.Unique

Cited by

1 results in Mathlib

Foundations

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

Assumes

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