Geometry of numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
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 p.28

source

theorem measure_theory.exists_pair_mem_lattice_not_disjoint_vadd {E : Type u_1} {L : Type u_2} [measurable_space E] {μ : measure_theory.measure E} {F s : set E} [add_comm_group L] [countable L] [add_action L E] [measurable_space L] [has_measurable_vadd L E] [measure_theory.vadd_invariant_measure L E μ] (fund : measure_theory.is_add_fundamental_domain L F μ) (hS : measure_theory.null_measurable_set s μ) (h : ⇑μ F < ⇑μ s) :

∃ (x 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 exists two distincts points x, y ∈ L such that (x + s) and (y + s) are not disjoint.

source

theorem measure_theory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure {E : Type u_1} [measurable_space E] {μ : measure_theory.measure E} {F s : set E} [normed_add_comm_group E] [normed_space ℝ E] [borel_space E] [finite_dimensional ℝ E] [μ.is_add_haar_measure] {L : add_subgroup E} [countable ↥L] (fund : measure_theory.is_add_fundamental_domain ↥L F μ) (h : ⇑μ F * 2 ^ fdim E < ⇑μ s) (h_symm : ∀ (x : E), x ∈ s → -x ∈ s) (h_conv : convex ℝ s) :

∃ (x : ↥L) (H : x ≠ 0), ↑x ∈ s

The Minkowksi 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.