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 AddSubgroup 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_2} [NormedAddCommGroup E] [MeasurableSpace E] (L : AddSubgroup 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

theorem Zlattice.covolume_eq_measure_fundamentalDomain {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : AddSubgroup 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 : AddSubgroup 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 : AddSubgroup 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 : AddSubgroup 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 : AddSubgroup (ι → ℝ)) [DiscreteTopology ↥L] [IsZlattice ℝ L] (b : Basis ι ℤ ↥L) : Zlattice.covolume L MeasureTheory.volume = |(Matrix.of (Subtype.val ∘ ⇑b)).det|