mulEquivHaarChar_eq — Mathlib

English

Let μ be a Haar measure on G which is regular. Then mulEquivHaarChar φ equals the scalar factor haarScalarFactor μ (μ.map φ).

Русский

Пусть μ — мера Хаара на G, регулярная. Тогда mulEquivHaarChar φ равно коэффициенту-скаляру haarScalarFactor μ (μ.map φ).

LaTeX

$$$mulEquivHaarChar(\phi) = haarScalarFactor\mu(\mu.map \phi)$$$

Lean4

@[to_additive]
theorem mulEquivHaarChar_eq (μ : Measure G) [IsHaarMeasure μ] [Regular μ] (φ : G ≃ₜ* G) :
    mulEquivHaarChar φ = haarScalarFactor μ (μ.map φ) :=
  by
  have smul := isMulLeftInvariant_eq_smul_of_regular haar μ
  unfold mulEquivHaarChar
  conv =>
    enter [1, 1]
    rw [smul]
  conv =>
    enter [1, 2, 2]
    rw [smul]
  simp_rw [MeasureTheory.Measure.map_smul]
  exact haarScalarFactor_smul_smul _ _ (haarScalarFactor_pos_of_isHaarMeasure haar μ).ne'

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