isMulLeftInvariant_haarMeasure — Mathlib

English

The Haar measure is left-invariant: for all g and measurable A, haarMeasure(gA)=haarMeasure(A).

Русский

Мера Хаара слева инвариантна: для любого g и измеримого A, haarMeasure(gA)=haarMeasure(A).

LaTeX

$$∀ g, haarMeasure_K0(gA) = haarMeasure_K0(A)$$

Lean4

@[to_additive]
instance isMulLeftInvariant_haarMeasure (K₀ : PositiveCompacts G) : IsMulLeftInvariant (haarMeasure K₀) :=
  by
  rw [← forall_measure_preimage_mul_iff]
  intro g A hA
  rw [haarMeasure_apply hA, haarMeasure_apply (measurable_const_mul g hA)]
    -- Porting note: Here was `congr 1`, but `to_additive` failed to generate a theorem.

  refine congr_arg (fun x : ℝ≥0∞ => x / (haarContent K₀).measure K₀) ?_
  apply Content.is_mul_left_invariant_outerMeasure
  apply is_left_invariant_haarContent

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