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 #


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