Documentation

TauCeti.NumberTheory.GeometryOfNumbers.LatticePointCount

Counting the lattice points of a dilated body, with a boundary-order error #

Let L be a ℤ-lattice in an n-dimensional real normed space E, let μ be an additive Haar measure on E, and let D be a bounded set whose frontier is Lipschitz parametrizable in dimension n - 1. When 0 < n, the resulting error is power-saving. Dilating D by c multiplies its volume by c ^ n, and each point of L in c • D accounts for one cell of the lattice, of volume covolume L μ. So

#(c • D ∩ L) = μ D / covolume L μ * c ^ n + O(c ^ (n - 1)) as c → ∞.

Mathlib's ZLattice.covolume.tendsto_card_div_pow' assumes only that the frontier of the body is null, which gives the limit but no error term at all. An error term is what a counting argument needs when the count is one term of a larger asymptotic, and it is what the stronger frontier hypothesis buys.

The argument #

Fix a fundamental domain F for L, and call w + F the cell at a lattice point w. The cells tile E, so the volume of a set X is squeezed between the total volume of the cells contained in X and the total volume of the cells meeting X, that is, between #A * μ F and #B * μ F where

A = {w ∈ L | w + F ⊆ X},   B = {w ∈ L | (w + F) ∩ X ≠ ∅}.

Since 0 ∈ F, a lattice point lies in its own cell, so A ⊆ X ∩ L ⊆ B and the count #(X ∩ L) is squeezed between the same two numbers. Both quantities therefore differ by at most #(B \ A) cells. A cell counted by B and not by A meets X and its complement; being convex it is preconnected, so it meets frontier X (IsPreconnected.inter_frontier_nonempty). Hence B \ A embeds in the lattice points of the thickened frontier frontier X + -F. That is abs_ncard_inter_mul_sub_measureReal_le, and it holds for any bounded X, with no regularity hypothesis on the frontier: the boundary term is not yet estimated, only identified.

Taking X = c • D and F the fundamental domain of a basis of L, the thickened frontier is c • frontier D + -F, whose lattice points number O(c ^ (n - 1)) by the boundary count TauCeti.IsLipschitzParametrizable.exists_ncard_smul_add_inter_le. This is the only place the Lipschitz hypothesis is used, and the only source of the error term.

Main results #

References #

source
theorem TauCeti.abs_ncard_inter_mul_sub_measureReal_le {E : Type u_1} [NormedAddCommGroup E] [ProperSpace E] [MeasurableSpace E] [BorelSpace E] {L : Submodule ℤ E} [DiscreteTopology ↥L] {μ : MeasureTheory.Measure E} [μ.IsAddRightInvariant] [MeasureTheory.IsLocallyFiniteMeasure μ] {F X : Set E} (hF₀ : 0 ∈ F) (hFpc : IsPreconnected F) (hFb : Bornology.IsBounded F) (hFm : MeasurableSet F) (hFu : ∀ (x w₁ : E), w₁ ∈ ↑L → ∀ w₂ ∈ ↑L, x - w₁ ∈ F → x - w₂ ∈ F → w₁ = w₂) (hFe : ∀ (x : E), ∃ w ∈ ↑L, x - w ∈ F) (hXb : Bornology.IsBounded X) :
|↑(X ∩ ↑L).ncard * μ.real F - μ.real X| ≤ ↑((frontier X + -F) ∩ ↑L).ncard * μ.real F

Counting lattice points by cells. Let F be a bounded measurable preconnected set containing 0 whose lattice translates w + F, for w in a discrete L, tile E. Then for every bounded set X the number of lattice points of X, weighted by the volume of F, differs from the volume of X by at most the volume of F times the number of lattice points in the thickened frontier frontier X + -F.

The hypotheses on F say exactly that it is a fundamental domain of the shape a counting argument uses: hFu and hFe are uniqueness and existence of the cell containing a point, hF₀ puts a lattice point in its own cell, and preconnectedness is what makes a cell straddling X meet its frontier. No regularity is asked of X, and none of frontier X: the boundary term is identified here and estimated by the caller.

source
theorem TauCeti.exists_abs_ncard_smul_inter_vadd_sub_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {D : Set E} (hDb : Bornology.IsBounded D) (hDfr : IsLipschitzParametrizable (Module.finrank ℝ E - 1) (frontier D)) :
∃ A ≥ 0, ∀ (ξ : E) (c : ℝ), 1 ≤ c → |↑(c • D ∩ (ξ +ᵥ ↑L)).ncard - μ.real D / ZLattice.covolume L μ * c ^ Module.finrank ℝ E| ≤ A * c ^ (Module.finrank ℝ E - 1)

Lattice points of a coset in a dilated body, uniformly in the coset. For a bounded set D whose frontier is Lipschitz parametrizable in dimension n - 1, the number of points of any coset ξ +ᵥ L lying in c • D is μ D / covolume L μ * c ^ n up to A * c ^ (n - 1), with A independent of both c ≥ 1 and the translate ξ.

Uniformity in ξ is the point, and it is not formal: the error is governed by the lattice cells meeting the boundary of the translated body, while a translate ranges over all of E, which is unbounded.

This is what lets a count be run over each coset of a sublattice with a single implied constant, as a count of ideals in a fixed ray class requires.

source
theorem TauCeti.isBigO_ncard_smul_inter_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {D : Set E} (hDb : Bornology.IsBounded D) (hDfr : IsLipschitzParametrizable (Module.finrank ℝ E - 1) (frontier D)) :
(fun (c : ℝ) => ↑(c • D ∩ ↑L).ncard - μ.real D / ZLattice.covolume L μ * c ^ Module.finrank ℝ E) =O[Filter.atTop] fun (c : ℝ) => c ^ (Module.finrank ℝ E - 1)

Lattice points in a dilated body, as an asymptotic statement: the count of the lattice points of c • D differs from μ D / covolume L μ * c ^ n by O(c ^ (n - 1)) as c → ∞.