addHaar_eq_volume — Mathlib

English

If μ is a Haar measure and you translate by g, the Haar character gives the relation to the new measure.

Русский

Если μ — мера Хаара и выполнить сдвиг на g, характер Хаара связывает новые и исходные меры.

LaTeX

$$$\\mathrm{distribHaarChar}(g) = \\dfrac{μ(g\\cdot S)}{μ(S)}$ (для подходящих S).$$

Lean4

/-- The Haar measure defined by any orthonormal basis of a finite-dimensional inner product space
is equal to its volume measure. -/
theorem addHaar_eq_volume {ι F : Type*} [Fintype ι] [NormedAddCommGroup F] [InnerProductSpace ℝ F]
    [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] (b : OrthonormalBasis ι ℝ F) :
    b.toBasis.addHaar = volume := by
  rw [Basis.addHaar_eq_iff]
  exact b.volume_parallelepiped

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