English
If the Minkowski bound of I is smaller than the volume of the convex LT region determined by f, then there exists a nonzero a in I such that w(a) < f(w) for every infinite place w.
Русский
Если граница Минковского по идеалу I меньше объема выпуклого региона LT, заданного f, то существует ненулевой элемент a ∈ I такой, что w(a) < f(w) для всех бесконечных место-вих w.
LaTeX
$$$\exists a \in I,\ a \neq 0 \ \land\ \forall w:\text{ InfinitePlace }K,\ w a < f w$$$
Lean4
/-- Let `I` be a fractional ideal of `K`. Assume that `f : InfinitePlace K → ℝ≥0` is such that
`minkowskiBound K I < volume (convexBodyLT K f)` where `convexBodyLT K f` is the set of
points `x` such that `‖x w‖ < f w` for all infinite places `w` (see `convexBodyLT_volume` for
the computation of this volume), then there exists a nonzero algebraic number `a` in `I` such
that `w a < f w` for all infinite places `w`. -/
theorem exists_ne_zero_mem_ideal_lt (h : minkowskiBound K I < volume (convexBodyLT K f)) :
∃ a ∈ (I : FractionalIdeal (𝓞 K)⁰ K), a ≠ 0 ∧ ∀ w : InfinitePlace K, w a < f w :=
by
have h_fund := ZSpan.isAddFundamentalDomain' (fractionalIdealLatticeBasis K I) volume
have : Countable (span ℤ (Set.range (fractionalIdealLatticeBasis K I))).toAddSubgroup :=
by
change Countable (span ℤ (Set.range (fractionalIdealLatticeBasis K I)))
infer_instance
obtain ⟨⟨x, hx⟩, h_nz, h_mem⟩ :=
exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure h_fund (convexBodyLT_neg_mem K f)
(convexBodyLT_convex K f) h
rw [mem_toAddSubgroup, mem_span_fractionalIdealLatticeBasis] at hx
obtain ⟨a, ha, rfl⟩ := hx
exact ⟨a, ha, by simpa using h_nz, (convexBodyLT_mem K f).mp h_mem⟩
