Covolume of ℤ-lattices #
Let E
be a finite dimensional real vector space with an inner product.
Let L
be a ℤ
-lattice L
defined as a discrete ℤ
-submodule of E
that spans E
over ℝ
.
Main definitions and results #
ZLattice.covolume
: the covolume ofL
defined as the volume of an arbitrary fundamental domain ofL
.ZLattice.covolume_eq_measure_fundamentalDomain
: the covolume ofL
does not depend on the choice of the fundamental domain ofL
.ZLattice.covolume_eq_det
: ifL
is a lattice inℝ^n
, then its covolume is the absolute value of the determinant of anyℤ
-basis ofL
.
def
ZLattice.covolume
{E : Type u_2}
[NormedAddCommGroup E]
[MeasurableSpace E]
(L : Submodule ℤ E)
(μ : autoParam (MeasureTheory.Measure E) _auto✝)
:
The covolume of a ℤ
-lattice is the volume of some fundamental domain; see
ZLattice.covolume_eq_volume
for the proof that the volume does not depend on the choice of
the fundamental domain.
Equations
- ZLattice.covolume L μ = (MeasureTheory.addCovolume (↥L) E μ).toReal
Instances For
theorem
ZLattice.covolume_eq_measure_fundamentalDomain
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[MeasurableSpace E]
[BorelSpace E]
(L : Submodule ℤ E)
[DiscreteTopology ↥L]
[IsZLattice ℝ L]
(μ : autoParam (MeasureTheory.Measure E) _auto✝)
[MeasureTheory.Measure.IsAddHaarMeasure μ]
{F : Set E}
(h : MeasureTheory.IsAddFundamentalDomain (↥L) F μ)
:
ZLattice.covolume L μ = (μ F).toReal
theorem
ZLattice.covolume_ne_zero
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[MeasurableSpace E]
[BorelSpace E]
(L : Submodule ℤ E)
[DiscreteTopology ↥L]
[IsZLattice ℝ L]
(μ : autoParam (MeasureTheory.Measure E) _auto✝)
[MeasureTheory.Measure.IsAddHaarMeasure μ]
:
ZLattice.covolume L μ ≠ 0
theorem
ZLattice.covolume_pos
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[MeasurableSpace E]
[BorelSpace E]
(L : Submodule ℤ E)
[DiscreteTopology ↥L]
[IsZLattice ℝ L]
(μ : autoParam (MeasureTheory.Measure E) _auto✝)
[MeasureTheory.Measure.IsAddHaarMeasure μ]
:
0 < ZLattice.covolume L μ
theorem
ZLattice.covolume_eq_det_mul_measure
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[MeasurableSpace E]
[BorelSpace E]
(L : Submodule ℤ E)
[DiscreteTopology ↥L]
[IsZLattice ℝ L]
(μ : autoParam (MeasureTheory.Measure E) _auto✝)
[MeasureTheory.Measure.IsAddHaarMeasure μ]
{ι : Type u_2}
[Fintype ι]
[DecidableEq ι]
(b : Basis ι ℤ ↥L)
(b₀ : Basis ι ℝ E)
:
ZLattice.covolume L μ = |b₀.det (Subtype.val ∘ ⇑b)| * (μ (ZSpan.fundamentalDomain b₀)).toReal
theorem
ZLattice.covolume_eq_det
{ι : Type u_2}
[Fintype ι]
[DecidableEq ι]
(L : Submodule ℤ (ι → ℝ))
[DiscreteTopology ↥L]
[IsZLattice ℝ L]
(b : Basis ι ℤ ↥L)
:
ZLattice.covolume L MeasureTheory.volume = |(Matrix.of (Subtype.val ∘ ⇑b)).det|