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

noncomputable def MeasureTheory.distribHaarChar {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 →* 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.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.distribHaarChar_apply {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) : (distribHaarChar A) g = (DomMulAct.mk g • Measure.addHaar).addHaarScalarFactor Measure.addHaar

theorem MeasureTheory.distribHaarChar_pos {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} : 0 < (distribHaarChar A) g

theorem MeasureTheory.addHaarScalarFactor_smul_eq_distribHaarChar {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] (g : G) : (DomMulAct.mk g • μ).addHaarScalarFactor μ = (distribHaarChar A) g

theorem MeasureTheory.addHaarScalarFactor_smul_inv_eq_distribHaarChar {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] (g : G) : μ.addHaarScalarFactor ((DomMulAct.mk g)⁻¹ • μ) = (distribHaarChar A) g

theorem MeasureTheory.addHaarScalarFactor_smul_eq_distribHaarChar_inv {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] (g : G) : μ.addHaarScalarFactor (DomMulAct.mk g • μ) = ((distribHaarChar A) g)⁻¹

theorem MeasureTheory.distribHaarChar_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] [MeasurableSpace A] [BorelSpace A] (μ : Measure A) [μ.IsAddHaarMeasure] [μ.Regular] (g : G) (s : Set A) : ↑((distribHaarChar A) g) * μ s = μ (g • s)

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) : (distribHaarChar A) g = r