English
The measure of the fundamental domain with Haar measure corresponds to the measure of the quotient space scaled by an invariant determinant.
Русский
Мера фундаментальной области по мере Хаара соответствует мере частного пространства, пропорциональной детерминанту базиса.
LaTeX
$$$\mu(\operatorname{fundamentalDomain}(b)) = \mu(\operatorname{FundamentalDomain}(b)) \,=\, \text{det}(b) \cdot \mu(\text{fundamentalDomain}(b_0)).$$$
Lean4
theorem measure_fundamentalDomain [Fintype ι] [DecidableEq ι] [MeasurableSpace E] (μ : Measure E) [BorelSpace E]
[Measure.IsAddHaarMeasure μ] (b₀ : Basis ι ℝ E) :
μ (fundamentalDomain b) = ENNReal.ofReal |b₀.det b| * μ (fundamentalDomain b₀) :=
by
have : FiniteDimensional ℝ E := FiniteDimensional.of_fintype_basis b
convert μ.addHaar_preimage_linearEquiv (b.equiv b₀ (Equiv.refl ι)) (fundamentalDomain b₀)
·
rw [Set.eq_preimage_iff_image_eq (LinearEquiv.bijective _), map_fundamentalDomain, Basis.map_equiv, Equiv.refl_symm,
Basis.reindex_refl]
· simp
