Theorems · Theorem · measure theory

MeasureTheory.Measure.measure_isAddInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop

∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsAddHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_8 : μ'.IsAddLeftInvariant]
  [μ.InnerRegularCompactLTTop] {s : Set G},
  MeasurableSet s → IsCompact (closure s) → μ' s = μ'.addHaarScalarFactor μ • μ 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 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, 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

TopologicalSpaceAddGroupIsTopologicalAddGroupMeasurableSpaceBorelSpaceLocallyCompactSpaceMeasureTheory.Measure.IsAddHaarMeasureMeasureTheory.IsFiniteMeasureOnCompactsMeasureTheory.Measure.IsAddLeftInvariantMeasureTheory.Measure.InnerRegularCompactLTTop