English
For a lattice L and a K-basis derived from it, the additive fundamental domain property holds with respect to any finite measure μ on the ambient space.
Русский
Для решётки L и базиса над K, полученного из неё, свойство аддитивной фундаментальной области сохраняется для любой меры μ на пространстве.
LaTeX
$$$\\IsAddFundamentalDomain(L, \\text{fundamentalDomain}(b.\\text{ofZLatticeBasis }\\mathbb{R}), \\mu)$$$
Lean4
theorem isAddFundamentalDomain {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
{L : Submodule ℤ E} [DiscreteTopology L] [IsZLattice ℝ L] [Finite ι] (b : Basis ι ℤ L) [MeasurableSpace E]
[OpensMeasurableSpace E] (μ : Measure E) : IsAddFundamentalDomain L (fundamentalDomain (b.ofZLatticeBasis ℝ)) μ :=
by
convert ZSpan.isAddFundamentalDomain (b.ofZLatticeBasis ℝ) μ
all_goals exact (b.ofZLatticeBasis_span ℝ).symm
