domSMul — Mathlib

English

If μ is a Haar measure on an additive group A and G acts by automorphisms on A, then the translated measure g • μ is again a Haar measure on A.

Русский

Если μ — мера Хаара на группе A, а G действуют на A через автоморфизмы, то сдвинутая мера g • μ снова является мерой Хаара на A.

LaTeX

$$$(g \\cdot \\mu) \\text{ isAddHaarMeasure}$$$

Lean4

instance domSMul {G A : Type*} [Group G] [AddCommGroup A] [DistribMulAction G A] [MeasurableSpace A]
    [TopologicalSpace A] [BorelSpace A] [IsTopologicalAddGroup A] [ContinuousConstSMul G A] {μ : Measure A}
    [μ.IsAddHaarMeasure] (g : Gᵈᵐᵃ) : (g • μ).IsAddHaarMeasure :=
  (DistribMulAction.toAddEquiv _ (DomMulAct.mk.symm g⁻¹)).isAddHaarMeasure_map _ (continuous_const_smul _)
    (continuous_const_smul _)

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