haarMeasure — Mathlib

English

Define Haar measure by normalizing the content: multiplying the content measure by the inverse of its mass on K0.

Русский

Определим меру Хаара как нормировку содержанием: массой контента на K0 делим по обратному значению массы.

LaTeX

$$haarMeasure_K0 = ((haarContent_K0).measure_K0)^{-1} · (haarContent_K0).measure$$

Lean4

/-- The Haar measure on the locally compact group `G`, scaled so that `haarMeasure K₀ K₀ = 1`. -/
@[to_additive /-- The Haar measure on the locally compact additive group `G`, scaled so that
    `addHaarMeasure K₀ K₀ = 1`. -/
    ]
noncomputable def haarMeasure (K₀ : PositiveCompacts G) : Measure G :=
  ((haarContent K₀).measure K₀)⁻¹ • (haarContent K₀).measure

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