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.

• ZLattice.covolume_div_covolume_eq_relIndex: Let L₁ be a sub-ℤ-lattice of L₂. Then the index of L₁ inside L₂ is equal to covolume L₁ / covolume L₂.

• ZLattice.covolume.tendsto_card_div_pow: Let s be a bounded measurable set of ι → ℝ, then the number of points in s ∩ n⁻¹ • L divided by n ^ card ι tends to volume s / covolume L when n : ℕ tends to infinity. See also ZLattice.covolume.tendsto_card_div_pow' for a version for InnerProductSpace ℝ E and ZLattice.covolume.tendsto_card_div_pow'' for the general version.

• ZLattice.covolume.tendsto_card_le_div: Let X be a cone in ι → ℝ and let F : (ι → ℝ) → ℝ be a function such that F (c • x) = c ^ card ι * F x. Then the number of points x ∈ X such that F x ≤ c divided by c tends to volume {x ∈ X | F x ≤ 1} / covolume L when c : ℝ tends to infinity. See also ZLattice.covolume.tendsto_card_le_div' for a version for InnerProductSpace ℝ E and ZLattice.covolume.tendsto_card_le_div'' for the general version.

Naming convention

Some results are true in the case where the ambient finite-dimensional real vector space is the pi-space ι → ℝ and in the case where it is an InnerProductSpace. We use the following convention: the plain name is for the pi case, for e.g. volume_image_eq_volume_div_covolume. For the same result in the InnerProductSpace case, we add a prime, for e.g. volume_image_eq_volume_div_covolume'. When the same result exists in the general case, we had two primes, e.g. covolume.tendsto_card_div_pow''.

noncomputable 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) [μ.IsAddHaarMeasure] {F : Set E} (h : MeasureTheory.IsAddFundamentalDomain (↥L) F μ) : covolume L μ = μ.real F

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

theorem ZLattice.covolume_eq_det_mul_measureReal {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) [μ.IsAddHaarMeasure] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℤ ↥L) (b₀ : Module.Basis ι ℝ E) : covolume L μ = |b₀.det (Subtype.val ∘ ⇑b)| * μ.real (ZSpan.fundamentalDomain b₀)

theorem ZLattice.covolume_eq_det {ι : Type u_2} [Fintype ι] [DecidableEq ι] (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology ↥L] [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L) : covolume L MeasureTheory.volume = |(Matrix.of (Subtype.val ∘ ⇑b)).det|

theorem ZLattice.covolume_eq_det_inv {ι : Type u_2} [Fintype ι] (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology ↥L] [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L) : covolume L MeasureTheory.volume = |↑(LinearEquiv.det (Module.Basis.ofZLatticeBasis ℝ L b).equivFun)|⁻¹

theorem ZLattice.covolume_div_covolume_eq_relIndex {ι : Type u_2} [Fintype ι] (L₁ L₂ : Submodule ℤ (ι → ℝ)) [DiscreteTopology ↥L₁] [IsZLattice ℝ L₁] [DiscreteTopology ↥L₂] [IsZLattice ℝ L₂] (h : L₁ ≤ L₂) : covolume L₁ MeasureTheory.volume / covolume L₂ MeasureTheory.volume = ↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup)

Let L₁ be a sub-ℤ-lattice of L₂. Then the index of L₁ inside L₂ is equal to covolume L₁ / covolume L₂.

theorem ZLattice.covolume_div_covolume_eq_relIndex' {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L₁ L₂ : Submodule ℤ E) [DiscreteTopology ↥L₁] [IsZLattice ℝ L₁] [DiscreteTopology ↥L₂] [IsZLattice ℝ L₂] (h : L₁ ≤ L₂) : covolume L₁ MeasureTheory.volume / covolume L₂ MeasureTheory.volume = ↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup)

A more general version of covolume_div_covolume_eq_relIndex; see the Naming conventions section in the introduction.

theorem ZLattice.volume_image_eq_volume_div_covolume {ι : Type u_2} [Fintype ι] (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology ↥L] [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L) {s : Set (ι → ℝ)} : MeasureTheory.volume (⇑(Module.Basis.ofZLatticeBasis ℝ L b).equivFun '' s) = MeasureTheory.volume s / ENNReal.ofReal (covolume L MeasureTheory.volume)

theorem ZLattice.volume_image_eq_volume_div_covolume' {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {ι : Type u_3} [Fintype ι] (b : Module.Basis ι ℤ ↥L) {s : Set E} (hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume) : MeasureTheory.volume (⇑(Module.Basis.ofZLatticeBasis ℝ L b).equivFun '' s) = MeasureTheory.volume s / ENNReal.ofReal (covolume L MeasureTheory.volume)

A more general version of ZLattice.volume_image_eq_volume_div_covolume; see the Naming conventions section in the introduction.

theorem ZLattice.covolume.tendsto_card_div_pow'' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] {ι : Type u_2} [Fintype ι] (b : Module.Basis ι ℤ ↥L) [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {s : Set E} (hs₁ : Bornology.IsBounded s) (hs₂ : MeasurableSet s) (hs₃ : MeasureTheory.volume (frontier (⇑(Module.Basis.ofZLatticeBasis ℝ L b).equivFun '' s)) = 0) : Filter.Tendsto (fun (n : ℕ) => ↑(Nat.card ↑(s ∩ (↑n)⁻¹ • ↑L)) / ↑n ^ Fintype.card ι) Filter.atTop (nhds (MeasureTheory.volume.real (⇑(Module.Basis.ofZLatticeBasis ℝ L b).equivFun '' s)))

A version of ZLattice.covolume.tendsto_card_div_pow for the general case; see the Naming convention section in the introduction.

theorem ZLattice.covolume.tendsto_card_le_div'' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] {ι : Type u_2} [Fintype ι] (b : Module.Basis ι ℤ ↥L) [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [Nonempty ι] {X : Set E} (hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X) {F : E → ℝ} (h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ Fintype.card ι * F x) (h₂ : Bornology.IsBounded {x : E | x ∈ X ∧ F x ≤ 1}) (h₃ : MeasurableSet {x : E | x ∈ X ∧ F x ≤ 1}) (h₄ : MeasureTheory.volume (frontier (⇑(Module.Basis.ofZLatticeBasis ℝ L b).equivFun '' {x : E | x ∈ X ∧ F x ≤ 1})) = 0) : Filter.Tendsto (fun (c : ℝ) => ↑(Nat.card ↑({x : E | x ∈ X ∧ F x ≤ c} ∩ ↑L)) / c) Filter.atTop (nhds (MeasureTheory.volume.real (⇑(Module.Basis.ofZLatticeBasis ℝ L b).equivFun '' {x : E | x ∈ X ∧ F x ≤ 1})))

A version of ZLattice.covolume.tendsto_card_le_div for the general case; see the Naming conventions section in the introduction.

theorem ZLattice.covolume.tendsto_card_div_pow {ι : Type u_1} [Fintype ι] (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology ↥L] [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L) {s : Set (ι → ℝ)} (hs₁ : Bornology.IsBounded s) (hs₂ : MeasurableSet s) (hs₃ : MeasureTheory.volume (frontier s) = 0) : Filter.Tendsto (fun (n : ℕ) => ↑(Nat.card ↑(s ∩ (↑n)⁻¹ • ↑L)) / ↑n ^ Fintype.card ι) Filter.atTop (nhds (MeasureTheory.volume.real s / covolume L MeasureTheory.volume))

theorem ZLattice.covolume.tendsto_card_le_div {ι : Type u_1} [Fintype ι] (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology ↥L] [IsZLattice ℝ L] {X : Set (ι → ℝ)} (hX : ∀ ⦃x : ι → ℝ⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X) {F : (ι → ℝ) → ℝ} (h₁ : ∀ (x : ι → ℝ) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ Fintype.card ι * F x) (h₂ : Bornology.IsBounded {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}) (h₃ : MeasurableSet {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}) (h₄ : MeasureTheory.volume (frontier {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}) = 0) [Nonempty ι] : Filter.Tendsto (fun (c : ℝ) => ↑(Nat.card ↑({x : ι → ℝ | x ∈ X ∧ F x ≤ c} ∩ ↑L)) / c) Filter.atTop (nhds (MeasureTheory.volume.real {x : ι → ℝ | x ∈ X ∧ F x ≤ 1} / covolume L MeasureTheory.volume))

theorem ZLattice.covolume.tendsto_card_div_pow' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {s : Set E} (hs₁ : Bornology.IsBounded s) (hs₂ : MeasurableSet s) (hs₃ : MeasureTheory.volume (frontier s) = 0) : Filter.Tendsto (fun (n : ℕ) => ↑(Nat.card ↑(s ∩ (↑n)⁻¹ • ↑L)) / ↑n ^ Module.finrank ℝ E) Filter.atTop (nhds (MeasureTheory.volume.real s / covolume L MeasureTheory.volume))

A version of ZLattice.covolume.tendsto_card_div_pow for the InnerProductSpace case; see the Naming convention section in the introduction.

theorem ZLattice.covolume.tendsto_card_le_div' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] [Nontrivial E] {X : Set E} {F : E → ℝ} (hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X) (h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ Module.finrank ℝ E * F x) (h₂ : Bornology.IsBounded {x : E | x ∈ X ∧ F x ≤ 1}) (h₃ : MeasurableSet {x : E | x ∈ X ∧ F x ≤ 1}) (h₄ : MeasureTheory.volume (frontier {x : E | x ∈ X ∧ F x ≤ 1}) = 0) : Filter.Tendsto (fun (c : ℝ) => ↑(Nat.card ↑({x : E | x ∈ X ∧ F x ≤ c} ∩ ↑L)) / c) Filter.atTop (nhds (MeasureTheory.volume.real {x : E | x ∈ X ∧ F x ≤ 1} / covolume L MeasureTheory.volume))

A version of ZLattice.covolume.tendsto_card_le_div for the InnerProductSpace case; see the Naming convention section in the introduction.