Modular character of a locally compact group

On a locally compact group, there is a natural homomorphism G → ℝ≥0*, which for g : G gives the value μ (· * g⁻¹) / μ, where μ is an (inner regular) Haar measure. This file defines this homomorphism, called the modular character, and shows that it is independent of the chosen Haar measure.

TODO: Show that the character is continuous.

Main Declarations

• modularCharacterFun: Define the modular character function. If μ is a left Haar measure on G and g : G, the measure A ↦ μ (A g⁻¹) is also a left Haar measure, so by uniqueness is of the form Δ(g) μ, for Δ(g) ∈ ℝ≥0. This Δ is the modular character. The result that this does not depend on the measure chosen is modularCharacterFun_eq_haarScalarFactor.
• modularCharacter: The homomorphism G →* ℝ≥0 whose toFun is modularCharacterFun.

noncomputable def MeasureTheory.Measure.modularCharacterFun {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [LocallyCompactSpace G] (g : G) : NNReal

The modular character as a map is g ↦ μ (· * g⁻¹) / μ, where μ is a left Haar measure.

See also modularCharacter that defines the map as a homomorphism.

noncomputable def MeasureTheory.Measure.addModularCharacterFun {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (g : G) : NNReal

The additive modular character as a map is g ↦ μ (· - g) / μ, where μ is an left additive Haar measure.

theorem MeasureTheory.Measure.modularCharacterFun_eq_haarScalarFactor {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsHaarMeasure] (g : G) : modularCharacterFun g = (map (fun (x : G) => x * g) μ).haarScalarFactor μ

Independence of modularCharacterFun from the chosen Haar measure.

theorem MeasureTheory.Measure.addModularCharacterFun_eq_addHaarScalarFactor {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsAddHaarMeasure] (g : G) : addModularCharacterFun g = (map (fun (x : G) => x + g) μ).addHaarScalarFactor μ

Independence of addModularCharacterFun from the chosen Haar measure

theorem MeasureTheory.Measure.map_right_mul_eq_modularCharacterFun_smul {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsHaarMeasure] [μ.InnerRegular] (g : G) : map (fun (x : G) => x * g) μ = modularCharacterFun g • μ

theorem MeasureTheory.Measure.map_right_add_eq_addModularCharacterFun_vadd {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsAddHaarMeasure] [μ.InnerRegular] (g : G) : map (fun (x : G) => x + g) μ = addModularCharacterFun g • μ

theorem MeasureTheory.Measure.modularCharacterFun_pos {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [LocallyCompactSpace G] (g : G) : 0 < modularCharacterFun g

theorem MeasureTheory.Measure.addModularCharacterFun_pos {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (g : G) : 0 < addModularCharacterFun g

theorem MeasureTheory.Measure.modularCharacterFun_map_one {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [LocallyCompactSpace G] : modularCharacterFun 1 = 1

theorem MeasureTheory.Measure.addModularCharacterFun_map_zero {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] : addModularCharacterFun 0 = 1

theorem MeasureTheory.Measure.modularCharacterFun_map_mul {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [LocallyCompactSpace G] (g h : G) : modularCharacterFun (g * h) = modularCharacterFun g * modularCharacterFun h

theorem MeasureTheory.Measure.addModularCharacterFun_map_add {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (g h : G) : addModularCharacterFun (g + h) = addModularCharacterFun g * addModularCharacterFun h

noncomputable def MeasureTheory.Measure.modularCharacter {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [LocallyCompactSpace G] : G →* NNReal

The modular character homomorphism. The underlying function is modularCharacterFun, which is g ↦ μ (· * g⁻¹) / μ, where μ is a left Haar measure.