map_right_mul_eq_modularCharacterFun_smul

English

The modular character equality with Haar scalar factor: modularCharacterFun g equals the Haar scalar factor of the corresponding left-translation map.

Русский

Неравенство модульной характеристики с фактором Хаара: modularCharacterFun g равно скалярному фактору Хаара отображения левого переноса.

LaTeX

$$modularCharacterFun g = haarScalarFactor (map (fun x => x * g) μ) μ$$

Lean4

@[to_additive]
theorem map_right_mul_eq_modularCharacterFun_smul [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [IsHaarMeasure μ]
    [InnerRegular μ] (g : G) : map (· * g) μ = modularCharacterFun g • μ :=
  by
  rw [modularCharacterFun_eq_haarScalarFactor μ _]
  exact isMulLeftInvariant_eq_smul_of_innerRegular _ μ

Похожие утверждения