English
A variant of Minkowski: with compact domain and discrete lattice, a nonzero lattice point exists under a relaxed inequality μF 2^finrank ≤ μs.
Русский
Вариант Минковского: при компактной области и дискретной решётке существует ненулевая точка решётки при ослабленном неравенстве.
LaTeX
$$Exists x ≠ 0 with x in L such that x ∈ s under h ≤ μs conditions.$$
Lean4
/-- The **Minkowski Convex Body Theorem for compact domain**. If `s` is a convex compact 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`. Compared to
`exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure`, this version requires in addition
that `s` is compact and `L` is discrete but provides a weaker inequality rather than a strict
inequality. -/
theorem exists_ne_zero_mem_lattice_of_measure_mul_two_pow_le_measure [NormedAddCommGroup E] [NormedSpace ℝ E]
[BorelSpace E] [FiniteDimensional ℝ E] [Nontrivial E] [IsAddHaarMeasure μ] {L : AddSubgroup E} [Countable L]
[DiscreteTopology L] (fund : IsAddFundamentalDomain L F μ) (h_symm : ∀ x ∈ s, -x ∈ s) (h_conv : Convex ℝ s)
(h_cpt : IsCompact s) (h : μ F * 2 ^ finrank ℝ E ≤ μ s) : ∃ x ≠ 0, ((x : L) : E) ∈ s :=
by
have h_mes : μ s ≠ 0 := by
intro hμ
suffices μ F = 0 from fund.measure_ne_zero (NeZero.ne μ) this
rw [hμ, le_zero_iff, mul_eq_zero] at h
exact h.resolve_right <| pow_ne_zero _ two_ne_zero
have h_nemp : s.Nonempty := nonempty_of_measure_ne_zero h_mes
let u : ℕ → ℝ≥0 := (exists_seq_strictAnti_tendsto 0).choose
let K : ConvexBody E := ⟨s, h_conv, h_cpt, h_nemp⟩
let S : ℕ → ConvexBody E := fun n => (1 + u n) • K
let Z : ℕ → Set E := fun n =>
(S n) ∩
(L \ {0})
-- The convex bodies `S n` have volume strictly larger than `μ s` and thus we can apply
-- `exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure` to them and obtain that
-- `S n` contains a nonzero point of `L`. Since the intersection of the `S n` is equal to `s`,
-- it follows that `s` contains a nonzero point of `L`.
have h_zero : 0 ∈ K := K.zero_mem_of_symmetric h_symm
suffices Set.Nonempty (⋂ n, Z n)
by
erw [← Set.iInter_inter, K.iInter_smul_eq_self h_zero] at this
· obtain ⟨x, hx⟩ := this
exact ⟨⟨x, by simp_all⟩, by aesop⟩
· exact (exists_seq_strictAnti_tendsto (0 : ℝ≥0)).choose_spec.2.2
have h_clos : IsClosed ((L : Set E) \ {0}) :=
by
rsuffices ⟨U, hU⟩ : ∃ U : Set E, IsOpen U ∧ U ∩ L = {0}
· rw [sdiff_eq_sdiff_iff_inf_eq_inf (z := U).mpr (by simp [Set.inter_comm .. ▸ hU.2, zero_mem])]
exact AddSubgroup.isClosed_of_discrete.sdiff hU.1
exact isOpen_inter_eq_singleton_of_mem_discrete (zero_mem L)
refine
IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed Z (fun n => ?_) (fun n => ?_)
((S 0).isCompact.inter_right h_clos) (fun n => (S n).isClosed.inter h_clos)
· refine Set.inter_subset_inter_left _ (SetLike.coe_subset_coe.mpr ?_)
refine ConvexBody.smul_le_of_le K h_zero ?_
rw [add_le_add_iff_left]
exact le_of_lt <| (exists_seq_strictAnti_tendsto (0 : ℝ≥0)).choose_spec.1 (Nat.lt.base n)
· suffices μ F * 2 ^ finrank ℝ E < μ (S n : Set E)
by
have h_symm' : ∀ x ∈ S n, -x ∈ S n := by
rintro _ ⟨y, hy, rfl⟩
exact ⟨-y, h_symm _ hy, by simp⟩
obtain ⟨x, hx_nz, hx_mem⟩ :=
exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure fund h_symm' (S n).convex this
exact ⟨x, hx_mem, by simp_all⟩
refine lt_of_le_of_lt h ?_
rw [ConvexBody.coe_smul', NNReal.smul_def, addHaar_smul_of_nonneg _ (NNReal.coe_nonneg _)]
rw [show μ s < _ ↔ 1 * μ s < _ by rw [one_mul]]
refine (mul_lt_mul_right h_mes (ne_of_lt h_cpt.measure_lt_top)).mpr ?_
rw [ofReal_pow (NNReal.coe_nonneg _)]
refine one_lt_pow₀ ?_ (ne_of_gt finrank_pos)
simp [u, (exists_seq_strictAnti_tendsto (0 : ℝ≥0)).choose_spec.2.1 n]
