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) : ∃ (x : L) (y : L), x ≠ y ∧ ¬Disjoint (x +ᵥ s) (y +ᵥ 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 ↥L] (fund : MeasureTheory.IsAddFundamentalDomain (↥L) F μ) (h_symm : ∀ x ∈ s, -x ∈ s) (h_conv : Convex ℝ s) (h : ↑↑μ F * 2 ^ FiniteDimensional.finrank ℝ E < ↑↑μ s) : ∃ (x : ↥L), x ≠ 0 ∧ ↑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.

theorem MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_le_measure {E : Type u_1} [MeasurableSpace E] {μ : MeasureTheory.Measure E} {F : Set E} {s : Set E} [NormedAddCommGroup E] [NormedSpace ℝ E] [BorelSpace E] [FiniteDimensional ℝ E] [Nontrivial E] [MeasureTheory.Measure.IsAddHaarMeasure μ] {L : AddSubgroup E} [Countable ↥L] [DiscreteTopology ↥L] (fund : MeasureTheory.IsAddFundamentalDomain (↥L) F μ) (h_symm : ∀ x ∈ s, -x ∈ s) (h_conv : Convex ℝ s) (h_cpt : IsCompact s) (h : ↑↑μ F * 2 ^ FiniteDimensional.finrank ℝ E ≤ ↑↑μ s) : ∃ (x : ↥L), x ≠ 0 ∧ ↑x ∈ s

The Minkowski Convex Body Theorem for compact domain. If s is a convex compact 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. Compared to exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure, this version requires in addition that s is compact and L is discrete but provides a weaker inequality rather than a strict inequality.