log_two_near_10 — Mathlib

English

|log 2 - 287209/414355| ≤ 10^-10

Русский

|log 2 - 287209/414355| ≤ 10^-10

LaTeX

$$$|\log 2 - \frac{287209}{414355}| \le 10^{-10}$$$

Lean4

theorem log_two_near_10 : |log 2 - 287209 / 414355| ≤ 1 / 10 ^ 10 :=
  by
  suffices |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
    by
    norm_num1 at *
    assumption
  have t : |(2⁻¹ : ℝ)| = 2⁻¹ := by rw [abs_of_pos]; norm_num
  have z := Real.abs_log_sub_add_sum_range_le (show |(2⁻¹ : ℝ)| < 1 by rw [t]; norm_num) 34
  rw [t] at z
  norm_num1 at z
  rw [one_div (2 : ℝ), log_inv, ← sub_eq_add_neg, _root_.abs_sub_comm] at z
  apply le_trans (_root_.abs_sub_le _ _ _) (add_le_add z _)
  simp_rw [sum_range_succ]
  norm_num

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