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 onG
andg : G
, the measureA ↦ μ (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 ismodularCharacterFun_eq_haarScalarFactor
.modularCharacter
: The homomorphism G →* ℝ≥0 whose toFun ismodularCharacterFun
.
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.
Equations
The additive modular character as a map is g ↦ μ (· - g) / μ
, where μ
is an
left additive Haar measure.
Equations
Independence of modularCharacterFun from the chosen Haar measure.
Independence of addModularCharacterFun from the chosen Haar measure
The modular character homomorphism. The underlying function is modularCharacterFun
, which is
g ↦ μ (· * g⁻¹) / μ
, where μ
is a left Haar measure.
Equations
- MeasureTheory.Measure.modularCharacter = { toFun := MeasureTheory.Measure.modularCharacterFun, map_one' := ⋯, map_mul' := ⋯ }