English
The modular-character map preserves multiplication: modularCharacterFun (g h) = modularCharacterFun g · modularCharacterFun h.
Русский
Модульная характеристика сохраняет умножение: modularCharacterFun (gh) = modularCharacterFun g · modularCharacterFun h.
LaTeX
$$modularCharacterFun (gh) = modularCharacterFun g \\cdot modularCharacterFun h$$
Lean4
@[to_additive]
theorem modularCharacterFun_map_mul (g h : G) :
modularCharacterFun (g * h) = modularCharacterFun g * modularCharacterFun h :=
by
borelize G
have mul_g_meas : Measurable (· * g) := Measurable.mul_const (fun ⦃_⦄ a ↦ a) g
have mul_h_meas : Measurable (· * h) := Measurable.mul_const (fun ⦃_⦄ a ↦ a) h
let ν := MeasureTheory.Measure.haar (G := G)
symm
calc
modularCharacterFun g * modularCharacterFun h = modularCharacterFun h * modularCharacterFun g := mul_comm _ _
_ = haarScalarFactor (map (· * h) (map (· * g) ν)) (map (· * g) ν) * modularCharacterFun g := by
rw [modularCharacterFun_eq_haarScalarFactor (map (· * g) ν) _]
_ = haarScalarFactor (map (· * h) (map (· * g) ν)) (map (· * g) ν) * haarScalarFactor (map (· * g) ν) ν := rfl
_ = haarScalarFactor (map (· * (g * h)) ν) ν := by
simp only [map_map mul_h_meas mul_g_meas, comp_mul_right, ← haarScalarFactor_eq_mul]
