Theorems · Definition · measure theory

MeasureTheory.distribHaarChar

{G : Type u_1} →
  (A : Type u_2) →
    [inst : Group G] →
      [inst_1 : AddCommGroup A] →
        [inst_2 : DistribMulAction G A] →
          [inst_3 : TopologicalSpace A] →
            [IsTopologicalAddGroup A] → [LocallyCompactSpace A] → [ContinuousConstSMul G A] → G →* NNReal

The distributive Haar character of a group G acting distributively on a group A is the unique positive real number Δ(g) such that μ (g • s) = Δ(g) * μ s for all Haar measures μ : Measure A, set s : Set A and g : G.

Defined in

Mathlib.MeasureTheory.Measure.Haar.DistribChar

Cited by

9 results in Mathlib

Foundations

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

Assumes

GroupAddCommGroupDistribMulActionTopologicalSpaceIsTopologicalAddGroupLocallyCompactSpaceContinuousConstSMul