mathlib3 documentation

measure_theory.group.geometry_of_numbers

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 #

TODO #

References #

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.

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.