four_zero_nine_six_lt_exp_sixteen

English

For N ≥ 1 and N ≤ 4096, (N)·exp(-4√(ln N)) ≤ 1.

Русский

Для N ≥ 1 и N ≤ 4096 выполняется (N) e^{−4√(ln N)} ≤ 1.

LaTeX

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

Lean4

theorem four_zero_nine_six_lt_exp_sixteen : 4096 < exp 16 :=
  by
  rw [← log_lt_iff_lt_exp (show (0 : ℝ) < 4096 by simp), show (4096 : ℝ) = 2 ^ 12 by norm_cast, ← rpow_natCast,
    log_rpow zero_lt_two, cast_ofNat]
  linarith [log_two_lt_d9]

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