Minkowski's theorem for the standard integer lattice in ℝⁿ #
This file specializes Minkowski's theorem on lattice points contained in convex
symmetric bodies to the standard integer lattice ℤⁿ ⊆ EuclideanSpace ℝ (Fin n).
The main result, classical_exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure,
states that a symmetric convex set of volume greater than 2 ^ n contains a nonzero
point all of whose coordinates are integers.
theorem
LeanPool.SumsThreeSquares.classical_exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure
{n : ℕ}
{s : Set (EuclideanSpace ℝ (Fin n))}
(h_symm : ∀ x ∈ s, -x ∈ s)
(h_conv : Convex ℝ s)
(h : 2 ^ n < MeasureTheory.volume s)
: