haarMeasure_self — Mathlib

English

The Haar measure on K0 assigns mass 1 to K0: haarMeasure K0 K0 = 1.

Русский

Мера Хаара на K0 придает массе K0 равной 1: haarMeasure K0 K0 = 1.

LaTeX

$$haarMeasure_K0(K0) = 1$$

Lean4

@[to_additive]
theorem haarMeasure_self {K₀ : PositiveCompacts G} : haarMeasure K₀ K₀ = 1 :=
  by
  haveI : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group
  simp only [haarMeasure, coe_smul, Pi.smul_apply, smul_eq_mul]
  rw [← K₀.isCompact.measure_closure, Content.measure_apply _ isClosed_closure.measurableSet, ENNReal.inv_mul_cancel]
  · exact (haarContent_outerMeasure_closure_pos K₀).ne'
  · exact (Content.outerMeasure_lt_top_of_isCompact _ K₀.isCompact.closure).ne

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