Documentation

Mathlib.MeasureTheory.Measure.Haar.DistribChar

The distributive character of Haar measures #

Given a group G acting by additive morphisms on a locally compact additive commutative group A, and an element g : G, one can pull back the Haar measure μ of A along the map (g • ·) : A → A to get another Haar measure μ' on A. By unicity of Haar measures, there exists some nonnegative real number r such that μ' = r • μ. We can thus define a map distribHaarChar : G → ℝ≥0 sending g to its associated real number r. Furthermore, this number doesn't depend on the Haar measure μ we started with, and distribHaarChar is a group homomorphism.

See also #

MeasureTheory.Measure.modularCharacter for the analogous definition when the action is multiplicative instead of distributive.

Zulip

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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem MeasureTheory.distribHaarChar_eq_div {G : Type u_1} {A : Type u_2} [Group G] [AddCommGroup A] [DistribMulAction G A] [TopologicalSpace A] [IsTopologicalAddGroup A] [LocallyCompactSpace A] [ContinuousConstSMul G A] [MeasurableSpace A] [BorelSpace A] {μ : Measure A} [μ.IsAddHaarMeasure] [μ.Regular] {s : Set A} (hs₀ : μ s 0) (hs : μ s ) (g : G) :
    ((distribHaarChar A) g) = μ (g s) / μ s
    theorem MeasureTheory.distribHaarChar_eq_of_measure_smul_eq_mul {G : Type u_1} {A : Type u_2} [Group G] [AddCommGroup A] [DistribMulAction G A] [TopologicalSpace A] [IsTopologicalAddGroup A] [LocallyCompactSpace A] [ContinuousConstSMul G A] {g : G} [MeasurableSpace A] [BorelSpace A] {μ : Measure A} [μ.IsAddHaarMeasure] [μ.Regular] {s : Set A} (hs₀ : μ s 0) (hs : μ s ) {r : NNReal} (hμgs : μ (g s) = r * μ s) :