Minkowski's convex body theorem for the integer lattice

Mathlib states Minkowski's convex body theorem for an arbitrary discrete subgroup with a fundamental domain. This file records its most common instance: the integer lattice ℤ^η in η → ℝ with Lebesgue measure, whose unit cube has volume one. The statement produces an integer vector directly, which is the form used in Diophantine approximation.

Main results

• MeasureTheory.exists_ne_zero_int_vec_mem_of_two_pow_le_volume: a compact convex symmetric set s ⊆ η → ℝ of volume at least 2 ^ |η| contains a nonzero integer vector.

theorem MeasureTheory.exists_ne_zero_int_vec_mem_of_two_pow_le_volume {η : Type u_1} [Fintype η] [Nonempty η] {s : Set (η → ℝ)} (h_symm : ∀ x ∈ s, -x ∈ s) (h_conv : Convex ℝ s) (h_cpt : IsCompact s) (h : 2 ^ Fintype.card η ≤ volume s) : ∃ (z : η → ℤ), z ≠ 0 ∧ (fun (k : η) => ↑(z k)) ∈ s

Minkowski's convex body theorem for the integer lattice. A compact convex set s ⊆ η → ℝ, symmetric about the origin, of volume at least 2 ^ |η| contains a nonzero integer vector.