English
Assume a fixed complex infinite place w0 and a bound h such that minkowskiBound(K,I) < volume(convexBodyLT'(K,f,w0)). Then there exists a nonzero a ∈ I with prescribed inequalities including bounds at all infinite places and an extra constraint at w0.
Русский
Пусть задано фиксированное комплексное бесконечное место w0 и предел h так, что minkowskiBound(K,I) < volume(convexBodyLT'(K,f,w0)). Тогда существует ненулевой a ∈ I с заданными неравенствами и дополнительными ограничениями на w0.
LaTeX
$$$\exists a \in I,\ a \neq 0 \wedge (\forall w, w \neq w_0 \Rightarrow w a < f w) \\ \wedge |(w_0.1 embedding(a)).re| < 1 \\wedge |(w_0.1 embedding(a)).im| < (f(w_0))^2$$$
Lean4
/-- A version of `exists_ne_zero_mem_ideal_lt` where the absolute value of the real part of `a` is
smaller than `1` at some fixed complex place. This is useful to ensure that `a` is not real. -/
theorem exists_ne_zero_mem_ideal_lt' (w₀ : { w : InfinitePlace K // IsComplex w })
(h : minkowskiBound K I < volume (convexBodyLT' K f w₀)) :
∃ a ∈ (I : FractionalIdeal (𝓞 K)⁰ K),
a ≠ 0 ∧
(∀ w : InfinitePlace K, w ≠ w₀ → w a < f w) ∧
|(w₀.val.embedding a).re| < 1 ∧ |(w₀.val.embedding a).im| < (f w₀ : ℝ) ^ 2 :=
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 w₀)
(convexBodyLT'_convex K f w₀) 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 w₀).mp h_mem⟩
