addHaarMeasure_eq_volume_pi — Mathlib

English

The Haar measure on the product piIcc01 for a finite index is equal to the product volume.

Русский

Мера Хаара на произведении piIcc01 равна произведению объёмов.

LaTeX

$$$\text{addHaarMeasure } \piIcc01(\iota) = \text{volume}$$$

Lean4

/-- The Haar measure equals the Lebesgue measure on `ℝ^ι`. -/
theorem addHaarMeasure_eq_volume_pi (ι : Type*) [Fintype ι] : addHaarMeasure (piIcc01 ι) = volume :=
  by
  convert (addHaarMeasure_unique volume (piIcc01 ι)).symm
  simp only [piIcc01, volume_pi_pi fun _ => Icc (0 : ℝ) 1, PositiveCompacts.coe_mk, Compacts.coe_mk,
    Finset.prod_const_one, ENNReal.ofReal_one, Real.volume_Icc, one_smul, sub_zero]

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