log_two_mul_two_le_sqrt_log_eight

English

The inequality 2/(1−2/e) ≤ 8 holds, giving a numerical bound used in the Behrend bound framework.

Русский

Неравенство 2/(1−2/e) ≤ 8 дает числовую границу для Бехрендовской оценки.

LaTeX

$$$ \\frac{2}{1 - \\frac{2}{e}} \\le 8 $$$

Lean4

theorem log_two_mul_two_le_sqrt_log_eight : log 2 * 2 ≤ √(log 8) :=
  by
  rw [show (8 : ℝ) = 2 ^ 3 by norm_num1, Real.log_pow, Nat.cast_ofNat]
  apply le_sqrt_of_sq_le
  rw [mul_pow, sq (log 2), mul_assoc, mul_comm]
  gcongr
  linarith only [log_two_lt_d9.le]

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