exp_four_lt — Mathlib

English

For N ∈ [2, 4096], (N)·exp(−4√(ln N)) ≤ 1.

Русский

Для N в диапазоне [2, 4096] выполняется (N) e^{−4√(ln N)} ≤ 1.

LaTeX

$$$$ N \\cdot \\exp(-4 \\sqrt{\\log N}) \\le 1 \\quad\\text{for } 2 \\le N \\le 4096. $$$$

Lean4

theorem exp_four_lt : exp 4 < 64 :=
  by
  rw [show (64 : ℝ) = 2 ^ ((6 : ℕ) : ℝ) by rw [rpow_natCast]; norm_num1, ←
    lt_log_iff_exp_lt (rpow_pos_of_pos zero_lt_two _), log_rpow zero_lt_two, ← div_lt_iff₀']
  · exact log_two_gt_d9.trans_le' (by norm_num1)
  · simp

Похожие утверждения