English
If |discr K| ≤ N, then the Minkowski bound for K is strictly less than boundOfDiscBdd N.
Русский
Если |дискр K| ≤ N, то минковский предел для K строго меньше boundOfDiscBdd N.
LaTeX
$$$$\\operatorname{minkowskiBound}(K, 1) < \\operatorname{boundOfDiscBdd}(N).$$$$
Lean4
/-- If `|discr K| ≤ N` then the degree of `K` is at most `rankOfDiscrBdd`. -/
theorem rank_le_rankOfDiscrBdd : finrank ℚ K ≤ rankOfDiscrBdd N :=
by
have h_nz : N ≠ 0 := by
refine fun h ↦ discr_ne_zero K ?_
rwa [h, Nat.cast_zero, abs_nonpos_iff] at hK
have h₂ : 1 < 3 * π / 4 :=
by
rw [_root_.lt_div_iff₀ (by positivity), ← _root_.div_lt_iff₀' (by positivity), one_mul]
linarith [Real.pi_gt_three]
obtain h | h := lt_or_ge 1 (finrank ℚ K)
· apply le_max_of_le_right
rw [Nat.le_floor_iff]
· have h := le_trans (abs_discr_ge h) (Int.cast_le.mpr hK)
contrapose! h
rw [← Real.rpow_natCast]
rw [Real.log_div_log] at h
refine
lt_of_le_of_lt ?_
(mul_lt_mul_of_pos_left (Real.rpow_lt_rpow_of_exponent_lt h₂ h) (by positivity : (0 : ℝ) < 4 / 9))
rw [Real.rpow_logb (lt_trans zero_lt_one h₂) (ne_of_gt h₂) (by positivity), ← mul_assoc, ← inv_div,
inv_mul_cancel₀ (by simp), one_mul, Int.cast_natCast]
· refine div_nonneg (Real.log_nonneg ?_) (Real.log_nonneg (le_of_lt h₂))
rw [mul_comm, ← mul_div_assoc, _root_.le_div_iff₀ (by positivity), one_mul, ← _root_.div_le_iff₀ (by positivity)]
exact le_trans (by norm_num) (Nat.one_le_cast.mpr (Nat.one_le_iff_ne_zero.mpr h_nz))
· exact le_max_of_le_left h
