Theorems · Definition · measure theory

MeasureTheory.Measure.addHaarScalarFactor

{G : Type u_1} →
  [inst : TopologicalSpace G] →
    [inst_1 : AddGroup G] →
      [IsTopologicalAddGroup G] →
        [inst_3 : MeasurableSpace G] →
          [BorelSpace G] →
            (μ' μ : MeasureTheory.Measure G) →
              [μ.IsAddHaarMeasure] → [MeasureTheory.IsFiniteMeasureOnCompacts μ'] → [μ'.IsAddLeftInvariant] → NNReal

Given two left-invariant measures which are finite on compacts, addHaarScalarFactor μ' μ is a scalar such that ∫ f dμ' = (addHaarScalarFactor μ' μ) ∫ f dμ for any compactly supported continuous function f. Note that there is a dissymmetry in the assumptions between μ' and μ: the measure μ' needs only be finite on compact sets, while μ has to be finite on compact sets and positive on open sets, i.e., an additive Haar measure, to exclude for instance the case where μ = 0, where the definition doesn't make sense.

Defined in

Mathlib.MeasureTheory.Measure.Haar.Unique

Cited by

58 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddGroupIsTopologicalAddGroupMeasurableSpaceBorelSpaceMeasureTheory.Measure.IsAddHaarMeasureMeasureTheory.IsFiniteMeasureOnCompactsMeasureTheory.Measure.IsAddLeftInvariant