English
Let K be a number field and let w1 be a distinguished infinite place. Given a nonzero algebraic integer x in 𝓞_K and a bound B with Minkowski data satisfied, there exists a nonzero y in 𝓞_K such that for every infinite place w different from w1, the value w(y) is strictly smaller than w(x), and the absolute norm |N_Q(y)| is at most B.
Русский
Пусть K — число поле, w1 — фиксированное бесконечное место. Для не нулевого целого числа x из 𝓞_K и заданного глобального порога B существует ненулевой элемент y из 𝓞_K такой, что для любого бесконечного места w ≠ w1 выполняется w(y) < w(x) и |N_Q(y)| ≤ B.
LaTeX
$$$\exists y \in \mathcal{O}_K, y \neq 0 \;\land\; (\forall w \neq w_1,\ w(y) < w(x)) \;\land\; |\mathrm{N}_{\mathbb{Q}}(y)| \le B$$$
Lean4
/-- This result shows that there always exists a next term in the sequence. -/
theorem seq_next {x : 𝓞 K} (hx : x ≠ 0) : ∃ y : 𝓞 K, y ≠ 0 ∧ (∀ w, w ≠ w₁ → w y < w x) ∧ |Algebra.norm ℚ (y : K)| ≤ B :=
by
have hx' := RingOfIntegers.coe_ne_zero_iff.mpr hx
let f : InfinitePlace K → ℝ≥0 := fun w ↦ ⟨(w x) / 2, div_nonneg (AbsoluteValue.nonneg _ _) (by simp)⟩
suffices ∀ w, w ≠ w₁ → f w ≠ 0 by
obtain ⟨g, h_geqf, h_gprod⟩ := adjust_f K B this
obtain ⟨y, h_ynz, h_yle⟩ :=
exists_ne_zero_mem_ringOfIntegers_lt K (f := g)
(by rw [convexBodyLT_volume]; convert hB; exact congr_arg ((↑) : NNReal → ENNReal) h_gprod)
refine ⟨y, h_ynz, fun w hw ↦ (h_geqf w hw ▸ h_yle w).trans ?_, ?_⟩
· rw [← Rat.cast_le (K := ℝ), Rat.cast_natCast]
calc
_ = ∏ w : InfinitePlace K, w (algebraMap _ K y) ^ mult w := (prod_eq_abs_norm (algebraMap _ K y)).symm
_ ≤ ∏ w : InfinitePlace K, (g w : ℝ) ^ mult w := by gcongr with w; exact (h_yle w).le
_ ≤ (B : ℝ) := by
simp_rw [← NNReal.coe_pow, ← NNReal.coe_prod]
exact le_of_eq (congr_arg toReal h_gprod)
· refine div_lt_self ?_ (by simp)
exact pos_iff.mpr hx'
intro _ _
rw [ne_eq, Nonneg.mk_eq_zero, div_eq_zero_iff, map_eq_zero, not_or]
exact ⟨hx', by simp⟩
