English
Definition of the Dedekind zeta residue as the explicit expression in terms of invariants.
Русский
Определение резидуала Dedekind zeta через явное выражение invariants.
LaTeX
$$$\mathrm{dedekindZeta\_residue}(K) = \dfrac{2^{nrRealPlaces(K)} (2\pi)^{nrComplexPlaces(K)} \mathrm{regulator}(K) \mathrm{classNumber}(K)}{\mathrm{torsionOrder}(K) \sqrt{|\mathrm{discr}(K)|}}$$$
Lean4
/-- The Minkowski lower bound `n^{2n}/((4/pi)^{2r_2}*n!^2)` for the absolute value of the discriminant
of a number field of degree n.
-/
theorem abs_discr_ge' :
(finrank ℚ K) ^ (2 * finrank ℚ K) / ((4 / π) ^ (2 * nrComplexPlaces K) * (finrank ℚ K).factorial ^ 2) ≤ |discr K| :=
by
-- We use `exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr` to get a nonzero
-- algebraic integer `x` of small norm and the fact that `1 ≤ |Norm x|` to get a lower bound
-- on `sqrt |discr K|`.
obtain ⟨x, h_nz, h_bd⟩ := exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr K
have h_nm : (1 : ℝ) ≤ |Algebra.norm ℚ (x : K)| :=
by
rw [← Algebra.coe_norm_int, ← Int.cast_one, ← Int.cast_abs, Rat.cast_intCast, Int.cast_le]
exact Int.one_le_abs (Algebra.norm_ne_zero_iff.mpr h_nz)
replace h_bd := le_trans h_nm h_bd
rwa [← inv_mul_le_iff₀, inv_div, mul_one, Real.le_sqrt (by positivity) (by positivity), ← Int.cast_abs, div_pow,
mul_pow, ← pow_mul, mul_comm _ 2, ← pow_mul, mul_comm _ 2] at h_bd
exact div_pos (by positivity) <| pow_pos (Nat.cast_pos.mpr finrank_pos) (finrank ℚ K)
