Theorems · Definition · measure theory

MeasureTheory.Measure.haarScalarFactor

{G : Type u_1} →
  [inst : TopologicalSpace G] →
    [inst_1 : Group G] →
      [IsTopologicalGroup G] →
        [inst_3 : MeasurableSpace G] →
          [BorelSpace G] →
            (μ' μ : MeasureTheory.Measure G) →
              [μ.IsHaarMeasure] → [MeasureTheory.IsFiniteMeasureOnCompacts μ'] → [μ'.IsMulLeftInvariant] → NNReal

Given two left-invariant measures which are finite on compacts, haarScalarFactor μ' μ is a scalar such that ∫ f dμ' = (haarScalarFactor μ' μ) ∫ 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., a 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

31 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceGroupIsTopologicalGroupMeasurableSpaceBorelSpaceMeasureTheory.Measure.IsHaarMeasureMeasureTheory.IsFiniteMeasureOnCompactsMeasureTheory.Measure.IsMulLeftInvariant