is_left_invariant_haarContent — Mathlib

English

haarContent is invariant under left translations: translating the compact set by any group element g leaves haarContent unchanged.

Русский

Содержание Хаара инвариантно относительно левых сдвигов: перенос множества по элементу группы g не меняет haarContent.

LaTeX

$$$\forall g\in G:\ \text{haarContent}_{K_0}(\mathrm{map}_{\llcorner g\llcorner}(K))=\text{haarContent}_{K_0}(K)$$$$

Lean4

/-- The variant of `is_left_invariant_chaar` for `haarContent` -/
@[to_additive /-- The variant of `is_left_invariant_addCHaar` for `addHaarContent` -/
    ]
theorem is_left_invariant_haarContent {K₀ : PositiveCompacts G} (g : G) (K : Compacts G) :
    haarContent K₀ (K.map _ <| continuous_mul_left g) = haarContent K₀ K := by
  simpa only [ENNReal.coe_inj, ← NNReal.coe_inj, haarContent_apply] using is_left_invariant_chaar g K

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