English
0 ≠ dedekindZeta_residue(K).
Русский
dedekindZeta_residue(K) ≠ 0.
LaTeX
$$\( \mathrm{dedekindZeta\_residue}(K) \neq 0 \)$$
Lean4
theorem abs_discr_ge (h : 1 < finrank ℚ K) : (4 / 9 : ℝ) * (3 * π / 4) ^ finrank ℚ K ≤ |discr K| :=
by
refine
le_trans ?_
(abs_discr_ge' K)
-- The sequence `a n` is a lower bound for `|discr K|`. We prove below by induction an uniform
-- lower bound for this sequence from which we deduce the result.
rw [mul_comm 2 _]
let a : ℕ → ℝ := fun n => (n : ℝ) ^ (n * 2) / ((4 / π) ^ n * (n.factorial : ℝ) ^ 2)
suffices ∀ n, 2 ≤ n → (4 / 9 : ℝ) * (3 * π / 4) ^ n ≤ a n
by
refine le_trans (this (finrank ℚ K) h) ?_
simp only [a]
gcongr
· exact (one_le_div Real.pi_pos).2 Real.pi_le_four
· rw [← card_add_two_mul_card_eq_rank, mul_comm]
exact Nat.le_add_left _ _
intro n hn
induction n, hn using Nat.le_induction with
| base => exact le_of_eq <| by simp [a, Nat.factorial_two]; field_simp; ring
| succ m _
h_m =>
suffices (3 : ℝ) ≤ (1 + 1 / m : ℝ) ^ (2 * m)
by
convert_to _ ≤ (a m) * (1 + 1 / m : ℝ) ^ (2 * m) / (4 / π)
· simp_rw [a, add_mul, one_mul, pow_succ, Nat.factorial_succ]
field_simp
simp [field, div_pow]
ring
· rw [_root_.le_div_iff₀ (by positivity), pow_succ]
convert (mul_le_mul h_m this (by positivity) (by positivity)) using 1
field_simp
refine le_trans (le_of_eq (by simp [field]; norm_num)) (one_add_mul_le_pow ?_ (2 * m))
exact le_trans (by norm_num : (-2 : ℝ) ≤ 0) (by positivity)
