English
Let I be a fractional ideal and B a real bound with Minkowski bound ≤ volume(convexBodySum(K,B)). Then there exists a ∈ I, a ≠ 0 with |N(a)| ≤ (B/d)^d.
Русский
Пусть I — дробный идеал, B — вещественное ограничение с Minkowski bound ≤ volume(convexBodySum(K,B)). Тогда существует a ∈ I, a ≠ 0, такое что |N(a)| ≤ (B/d)^d.
LaTeX
$$$\exists a \in I,\ a \neq 0 \land |\operatorname{Norm}_{\mathbb{Q}}(a)| \le (\frac{B}{\operatorname{finrank}_{\mathbb{Q}}K})^{\operatorname{finrank}_{\mathbb{Q}}K}$$$
Lean4
/-- Let `I` be a fractional ideal of `K`. Assume that `B : ℝ` is such that
`minkowskiBound K I < volume (convexBodySum K B)` where `convexBodySum K B` is the set of points
`x` such that `∑ w real, ‖x w‖ + 2 * ∑ w complex, ‖x w‖ ≤ B` (see `convexBodySum_volume` for
the computation of this volume), then there exists a nonzero algebraic number `a` in `I` such
that `|Norm a| < (B / d) ^ d` where `d` is the degree of `K`. -/
theorem exists_ne_zero_mem_ideal_of_norm_le {B : ℝ} (h : (minkowskiBound K I) ≤ volume (convexBodySum K B)) :
∃ a ∈ (I : FractionalIdeal (𝓞 K)⁰ K), a ≠ 0 ∧ |Algebra.norm ℚ (a : K)| ≤ (B / finrank ℚ K) ^ finrank ℚ K :=
by
have hB : 0 ≤ B := by
contrapose! h
rw [convexBodySum_volume_eq_zero_of_le_zero K (le_of_lt h)]
exact minkowskiBound_pos K I
have h1 : 0 < (finrank ℚ K : ℝ)⁻¹ := inv_pos.mpr (Nat.cast_pos.mpr finrank_pos)
have h2 : 0 ≤ B / (finrank ℚ K) := div_nonneg hB (Nat.cast_nonneg _)
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_le_measure h_fund (fun _ ↦ convexBodySum_neg_mem K B)
(convexBodySum_convex K B) (convexBodySum_compact K B) h
rw [mem_toAddSubgroup, mem_span_fractionalIdealLatticeBasis] at hx
obtain ⟨a, ha, rfl⟩ := hx
refine ⟨a, ha, by simpa using h_nz, ?_⟩
rw [← rpow_natCast, ← rpow_le_rpow_iff (by simp only [Rat.cast_abs, abs_nonneg]) (rpow_nonneg h2 _) h1, ← rpow_mul h2,
mul_inv_cancel₀ (Nat.cast_ne_zero.mpr (ne_of_gt finrank_pos)), rpow_one,
le_div_iff₀' (Nat.cast_pos.mpr finrank_pos)]
refine le_trans ?_ ((convexBodySum_mem K B).mp h_mem)
rw [← le_div_iff₀' (Nat.cast_pos.mpr finrank_pos), ← sum_mult_eq, Nat.cast_sum]
refine
le_trans ?_
(geom_mean_le_arith_mean Finset.univ _ _ (fun _ _ => Nat.cast_nonneg _) ?_ (fun _ _ => AbsoluteValue.nonneg _ _))
· simp_rw [← prod_eq_abs_norm, rpow_natCast]
exact le_of_eq rfl
· rw [← Nat.cast_sum, sum_mult_eq, Nat.cast_pos]
exact finrank_pos
