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 { x : E // x ∈ 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 { x : E // x ∈ L }] [IsZLattice ℝ L] (μ : autoParam (MeasureTheory.Measure E) _auto✝) [MeasureTheory.Measure.IsAddHaarMeasure μ] {F : Set E} (h : MeasureTheory.IsAddFundamentalDomain { x : E // x ∈ 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 { x : E // x ∈ 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 { x : E // x ∈ 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 { x : E // x ∈ L }] [IsZLattice ℝ L] (μ : autoParam (MeasureTheory.Measure E) _auto✝) [MeasureTheory.Measure.IsAddHaarMeasure μ] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Basis ι ℤ { x : E // x ∈ 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 { x : ι → ℝ // x ∈ L }] [IsZLattice ℝ L] (b : Basis ι ℤ { x : ι → ℝ // x ∈ L }) : ZLattice.covolume L MeasureTheory.volume = |(Matrix.of (Subtype.val ∘ ⇑b)).det|