English
For any invertible fractional ideal I, there exists a nonzero a ∈ I with a norm bound: |N(a)| ≤ absNorm(I) times a fixed Minkowski-type factor times sqrt(|discr(K)|).
Русский
Для любого обратимого дробного идеала I существует не нулевой элемент a ∈ I с ограничением по норме: |N(a)| ≤ absNorm(I) × константа Минковского × sqrt(|discr(K)|).
LaTeX
$$$\exists a \in I,\ a \neq 0 \land |\mathrm{Algebra.norm}_{\mathbb{Q}}(a)| \\le \mathrm{absNorm}(I) \cdot (4/\pi)^{nrComplexPlaces(K)} \cdot \dfrac{(\mathrm{finrank}\mathbb{Q}K)!}{(\mathrm{finrank}\mathbb{Q}K)^{\mathrm{finrank}\mathbb{Q}K}} \cdot \sqrt{|\mathrm{discr}(K)|}$$$
Lean4
theorem exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ) :
∃ a ∈ (I : FractionalIdeal (𝓞 K)⁰ K),
a ≠ 0 ∧
|Algebra.norm ℚ (a : K)| ≤
FractionalIdeal.absNorm I.1 * (4 / π) ^ nrComplexPlaces K * (finrank ℚ K).factorial /
(finrank ℚ K) ^ (finrank ℚ K) *
Real.sqrt |discr K| :=
by
classical
-- The smallest possible value for `exists_ne_zero_mem_ideal_of_norm_le`
let B := (minkowskiBound K I * (convexBodySumFactor K)⁻¹).toReal ^ (1 / (finrank ℚ K : ℝ))
have h_le : (minkowskiBound K I) ≤ volume (convexBodySum K B) :=
by
refine le_of_eq ?_
rw [convexBodySum_volume, ← ENNReal.ofReal_pow (by positivity), ← Real.rpow_natCast, ← Real.rpow_mul toReal_nonneg,
div_mul_cancel₀, Real.rpow_one, ofReal_toReal, mul_comm, mul_assoc, ← coe_mul,
inv_mul_cancel₀ (convexBodySumFactor_ne_zero K), ENNReal.coe_one, mul_one]
· exact mul_ne_top (ne_of_lt (minkowskiBound_lt_top K I)) coe_ne_top
· exact (Nat.cast_ne_zero.mpr (ne_of_gt finrank_pos))
convert exists_ne_zero_mem_ideal_of_norm_le K I h_le
rw [div_pow B, ← Real.rpow_natCast B, ← Real.rpow_mul (by positivity),
div_mul_cancel₀ _ (Nat.cast_ne_zero.mpr <| ne_of_gt finrank_pos), Real.rpow_one, mul_comm_div, mul_div_assoc']
congr 1
rw [eq_comm]
calc
_ =
FractionalIdeal.absNorm I.1 * (2 : ℝ)⁻¹ ^ nrComplexPlaces K * sqrt ‖discr K‖₊ * (2 : ℝ) ^ finrank ℚ K *
((2 : ℝ) ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / (Nat.factorial (finrank ℚ K)))⁻¹ :=
by
simp_rw [minkowskiBound, convexBodySumFactor, volume_fundamentalDomain_fractionalIdealLatticeBasis,
volume_fundamentalDomain_latticeBasis, toReal_mul, toReal_pow, toReal_inv, coe_toReal, toReal_ofNat,
mixedEmbedding.finrank, mul_assoc]
rw [ENNReal.toReal_ofReal (Rat.cast_nonneg.mpr (FractionalIdeal.absNorm_nonneg I.1))]
simp_rw [NNReal.coe_inv, NNReal.coe_div, NNReal.coe_mul, NNReal.coe_pow, NNReal.coe_div, coe_real_pi,
NNReal.coe_ofNat, NNReal.coe_natCast]
_ =
FractionalIdeal.absNorm I.1 *
(2 : ℝ) ^ (finrank ℚ K - nrComplexPlaces K - nrRealPlaces K + nrComplexPlaces K : ℤ) *
Real.sqrt ‖discr K‖ *
Nat.factorial (finrank ℚ K) *
π⁻¹ ^ (nrComplexPlaces K) :=
by
simp_rw [inv_div, div_eq_mul_inv, mul_inv, ← zpow_neg_one, ← zpow_natCast, mul_zpow, ← zpow_mul, neg_one_mul,
mul_neg_one, neg_neg, Real.coe_sqrt, coe_nnnorm, sub_eq_add_neg, zpow_add₀ (two_ne_zero : (2 : ℝ) ≠ 0)]
ring
_ =
FractionalIdeal.absNorm I.1 * (2 : ℝ) ^ (2 * nrComplexPlaces K : ℤ) * Real.sqrt ‖discr K‖ *
Nat.factorial (finrank ℚ K) *
π⁻¹ ^ (nrComplexPlaces K) :=
by
congr
rw [← card_add_two_mul_card_eq_rank, Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat]
ring
_ = FractionalIdeal.absNorm I.1 * (4 / π) ^ nrComplexPlaces K * (finrank ℚ K).factorial * Real.sqrt |discr K| :=
by
rw [Int.norm_eq_abs, zpow_mul, show (2 : ℝ) ^ (2 : ℤ) = 4 by norm_cast, div_pow, inv_eq_one_div, div_pow, one_pow,
zpow_natCast]
ring
