mulEquivHaarChar_smul_eq_comap — Mathlib

English

For Haar measure μ, the scaled measure equals the comapφ of μ: mulEquivHaarChar φ · μ = μ comap φ.

Русский

Для меры Хаара μ масштабированная мера равна комап μ по φ: mulEquivHaarChar φ · μ = μ.comap φ.

LaTeX

$$$mulEquivHaarChar(\phi) \cdot μ = μ.map \?$$$

Lean4

@[to_additive addEquivAddHaarChar_smul_eq_comap]
theorem mulEquivHaarChar_smul_eq_comap (μ : Measure G) [IsHaarMeasure μ] [Regular μ] (φ : G ≃ₜ* G) :
    (mulEquivHaarChar φ) • μ = μ.comap φ :=
  by
  let e := φ.toHomeomorph.toMeasurableEquiv
  rw [show ⇑φ = ⇑e from rfl, ← e.map_symm, show ⇑e.symm = ⇑φ.symm from rfl]
  have : (map (φ.symm) μ).Regular := Regular.map φ.symm.toHomeomorph
  rw [← mulEquivHaarChar_smul_map (map φ.symm μ) φ, map_map]
  · simp
  · fun_prop
  · fun_prop

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