English
Let μ be a left-invariant measure on a finite-dimensional real space E and b a basis. Then μ equals the Haar measure defined by b if and only if μ assigns volume 1 to the parallelepiped P(b).
Русский
Пусть μ — левая инвариантная мера на конечномерном вещественном пространстве E и дан базис b. Тогда μ равна мере Хаара, заданной базисом b, тогда и только тогда, когда μ присваивает объему 1 параллелепипеду P(b).
LaTeX
$$$(b.addHaar = \mu) \iff (\mu( b.parallelepiped ) = 1)$$$
Lean4
/-- Let `μ` be a σ-finite left invariant measure on `E`. Then `μ` is equal to the Haar measure
defined by `b` iff the parallelepiped defined by `b` has measure `1` for `μ`. -/
theorem addHaar_eq_iff [SecondCountableTopology E] (b : Basis ι ℝ E) (μ : Measure E) [SigmaFinite μ]
[IsAddLeftInvariant μ] : b.addHaar = μ ↔ μ b.parallelepiped = 1 :=
by
rw [Basis.addHaar_def]
exact addHaarMeasure_eq_iff b.parallelepiped μ
