Covolume of ℤ-lattices

Let E be a finite dimensional real vector space.

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 of L defined as the volume of an arbitrary fundamental domain of L.

• ZLattice.covolume_eq_measure_fundamentalDomain: the covolume of L does not depend on the choice of the fundamental domain of L.

• ZLattice.covolume_eq_det: if L is a lattice in ℝ^n, then its covolume is the absolute value of the determinant of any ℤ-basis of L.

def ZLattice.covolume {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] (L : Submodule ℤ E) (μ : MeasureTheory.Measure E := by volume_tac) : ℝ

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

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] (μ : MeasureTheory.Measure E := by volume_tac) [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] (μ : MeasureTheory.Measure E := by volume_tac) [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] (μ : MeasureTheory.Measure E := by volume_tac) [MeasureTheory.Measure.IsAddHaarMeasure μ] : 0 < ZLattice.covolume L μ

theorem ZLattice.covolume_comap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (μ : MeasureTheory.Measure E := by volume_tac) [MeasureTheory.Measure.IsAddHaarMeasure μ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] (ν : MeasureTheory.Measure F := by volume_tac) [MeasureTheory.Measure.IsAddHaarMeasure ν] {e : F ≃L[ℝ] E} (he : MeasureTheory.MeasurePreserving (⇑e) ν μ) : ZLattice.covolume (ZLattice.comap ℝ L ↑e.toLinearEquiv) ν = 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] (μ : MeasureTheory.Measure E := by volume_tac) [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|