English
The fundamental domain is almost everywhere equal to the parallelepiped associated to b with respect to Haar measure.
Русский
Фундаментальная область почти везде равна параллелепипеду, ассоциированному с b по мере Хаара.
LaTeX
$$$\operatorname{fundamentalDomain}(b) =^{\text{ae}} \operatorname{parallelepiped}(\operatorname{coeff}(b)).$$$
Lean4
theorem fundamentalDomain_ae_parallelepiped [Fintype ι] [MeasurableSpace E] (μ : Measure E) [BorelSpace E]
[Measure.IsAddHaarMeasure μ] : fundamentalDomain b =ᵐ[μ] parallelepiped b := by
classical
have : FiniteDimensional ℝ E := FiniteDimensional.of_fintype_basis b
rw [← measure_symmDiff_eq_zero_iff, symmDiff_of_le (fundamentalDomain_subset_parallelepiped b)]
suffices (parallelepiped b \ fundamentalDomain b) ⊆ ⋃ i, AffineSubspace.mk' (b i) (span ℝ (b '' (Set.univ \ { i })))
by
refine measure_mono_null this (measure_iUnion_null_iff.mpr fun i ↦ Measure.addHaar_affineSubspace μ _ ?_)
refine (ne_of_mem_of_not_mem' (AffineSubspace.mem_top _ _ 0) (AffineSubspace.mem_mk'.not.mpr ?_)).symm
simp_rw [vsub_eq_sub, zero_sub, neg_mem_iff]
exact linearIndependent_iff_notMem_span.mp b.linearIndependent i
intro x hx
simp_rw [parallelepiped_basis_eq, Set.mem_Icc, Set.mem_diff, Set.mem_setOf_eq, mem_fundamentalDomain, Set.mem_Ico,
not_forall, not_and, not_lt] at hx
obtain ⟨i, hi⟩ := hx.2
have : b.repr x i = 1 := le_antisymm (hx.1 i).2 (hi (hx.1 i).1)
rw [← b.sum_repr x, ← Finset.sum_erase_add _ _ (Finset.mem_univ i), this, one_smul, ← vadd_eq_add]
refine Set.mem_iUnion.mpr ⟨i, AffineSubspace.vadd_mem_mk' _ (sum_smul_mem _ _ (fun i hi ↦ Submodule.subset_span ?_))⟩
exact ⟨i, Set.mem_diff_singleton.mpr ⟨trivial, Finset.ne_of_mem_erase hi⟩, rfl⟩
