haarMeasure_apply — Mathlib

English

For any measurable set s, the Haar measure of s equals the outer measure of s divided by the mass of K0 under haarContent.

Русский

Для любого измеримого множества s мера Хаара от s равна внешней мере s деленной на массу K0 по haarContent.

LaTeX

$$haarmeasure_K0(s) = haarContent_K0.outerMeasure(s) / haarContent_K0.measure(K0)$$

Lean4

@[to_additive]
theorem haarMeasure_apply {K₀ : PositiveCompacts G} {s : Set G} (hs : MeasurableSet s) :
    haarMeasure K₀ s = (haarContent K₀).outerMeasure s / (haarContent K₀).measure K₀ :=
  by
  change ((haarContent K₀).measure K₀)⁻¹ * (haarContent K₀).measure s = _
  simp only [hs, div_eq_mul_inv, mul_comm, Content.measure_apply]

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