English
Independence of modularCharacterFun from the chosen Haar measure: for any g ∈ G, modularCharacterFun g equals the Haar scalar factor of the map by left multiplication by g.
Русский
Независимость modularCharacterFun от выбранной меры Хаара: для любого g ∈ G modularCharacterFun g равно скалярному фактору Хаара от отображения левого умножения на g.
LaTeX
$$modularCharacterFun g = haarScalarFactor (map (· * g) μ) μ$$
Lean4
/-- 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. -/
@[to_additive /-- The additive modular character as a map is `g ↦ μ (· - g) / μ`, where `μ` is an
left additive Haar measure. -/
]
noncomputable def modularCharacterFun (g : G) : ℝ≥0 :=
letI : MeasurableSpace G := borel G
haveI : BorelSpace G := ⟨rfl⟩
haarScalarFactor (map (· * g) MeasureTheory.Measure.haar) MeasureTheory.Measure.haar
