English
If s is a convex, compact, symmetric domain in E and its volume is large relative to the covolume of a lattice L, then s contains a nonzero lattice point of L (under a weaker inequality than the strict one).
Русский
Если s — выпуклая компактная симметричная область, её объём велик по отношению к ковольюму решётки L, то s содержит ненулевую точку решётки.
LaTeX
$$$\\exists x \\in L\\setminus\\{0\\}, x \\in s.$$$
Lean4
/-- 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`. -/
theorem exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure [NormedAddCommGroup E] [NormedSpace ℝ E]
[BorelSpace E] [FiniteDimensional ℝ E] [IsAddHaarMeasure μ] {L : AddSubgroup E} [Countable L]
(fund : IsAddFundamentalDomain L F μ) (h_symm : ∀ x ∈ s, -x ∈ s) (h_conv : Convex ℝ s)
(h : μ F * 2 ^ finrank ℝ E < μ s) : ∃ x ≠ 0, ((x : L) : E) ∈ s :=
by
have h_vol : μ F < μ ((2⁻¹ : ℝ) • s) :=
by
rw [addHaar_smul_of_nonneg μ (by simp : 0 ≤ (2 : ℝ)⁻¹) s, ←
mul_lt_mul_right (pow_ne_zero (finrank ℝ E) (two_ne_zero' _)) (by finiteness), mul_right_comm,
ofReal_pow (by simp : 0 ≤ (2 : ℝ)⁻¹), ofReal_inv_of_pos zero_lt_two]
norm_num
rwa [← mul_pow, ENNReal.inv_mul_cancel two_ne_zero ofNat_ne_top, one_pow, one_mul]
obtain ⟨x, y, hxy, h⟩ := exists_pair_mem_lattice_not_disjoint_vadd fund ((h_conv.smul _).nullMeasurableSet _) h_vol
obtain ⟨_, ⟨v, hv, rfl⟩, w, hw, hvw⟩ := Set.not_disjoint_iff.mp h
refine ⟨x - y, sub_ne_zero.2 hxy, ?_⟩
rw [Set.mem_inv_smul_set_iff₀ (two_ne_zero' ℝ)] at hv hw
simp_rw [AddSubgroup.vadd_def, vadd_eq_add, add_comm _ w, ← sub_eq_sub_iff_add_eq_add, ← AddSubgroup.coe_sub] at hvw
rw [← hvw, ← inv_smul_smul₀ (two_ne_zero' ℝ) (_ - _), smul_sub, sub_eq_add_neg, smul_add]
refine h_conv hw (h_symm _ hv) ?_ ?_ ?_ <;> norm_num
