Geometry of numbers #
In this file we prove some of the fundamental theorems in the geometry of numbers, as studied by Hermann Minkowski.
Main results #
exists_pair_mem_lattice_not_disjoint_vadd: Blichfeldt's principle, existence of two distinct points in a subgroup such that the translates of a set by these two points are not disjoint when the covolume of the subgroup is larger than the volume of the set.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure: Minkowski's theorem, existence of a non-zero lattice point inside a convex symmetric domain of large enough volume.
TODO #
- Calculate the volume of the fundamental domain of a finite index subgroup
- Voronoi diagrams
- See Pete L. Clark, Abstract Geometry of Numbers: Linear Forms (arXiv) for some more ideas.
References #
- [Pete L. Clark, Geometry of Numbers with Applications to Number Theory][clark_gon] p.28
theorem
MeasureTheory.exists_pair_mem_lattice_not_disjoint_vadd
{E : Type u_1}
{L : Type u_2}
[MeasurableSpace E]
{μ : MeasureTheory.Measure E}
{F : Set E}
{s : Set E}
[AddCommGroup L]
[Countable L]
[AddAction L E]
[MeasurableSpace L]
[MeasurableVAdd L E]
[MeasureTheory.VAddInvariantMeasure L E μ]
(fund : MeasureTheory.IsAddFundamentalDomain L F)
(hS : MeasureTheory.NullMeasurableSet s)
(h : ↑↑μ F < ↑↑μ s)
:
Blichfeldt's Theorem. If the volume of the set s is larger than the covolume of the
countable subgroup L of E, then there exist two distinct points x, y ∈ L such that (x + s)
and (y + s) are not disjoint.
theorem
MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure
{E : Type u_1}
[MeasurableSpace E]
{μ : MeasureTheory.Measure E}
{F : Set E}
{s : Set E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[BorelSpace E]
[FiniteDimensional ℝ E]
[MeasureTheory.Measure.IsAddHaarMeasure μ]
{L : AddSubgroup E}
[Countable { x // x ∈ L }]
(fund : MeasureTheory.IsAddFundamentalDomain { x // x ∈ L } F)
(h : ↑↑μ F * 2 ^ FiniteDimensional.finrank ℝ E < ↑↑μ s)
(h_symm : ∀ (x : E), x ∈ s → -x ∈ s)
(h_conv : Convex ℝ s)
:
∃ x x_1, ↑x ∈ s
The Minkowski Convex Body Theorem. If s is a convex symmetric domain of E whose volume
is large enough compared to the covolume of a lattice L of E, then it contains a non-zero
lattice point of L.