exp_one_near_10 — Mathlib

English

There exists a rational r = 2244083/825552 with |exp(1) - r| ≤ 10^-10.

Русский

Существует рациональное число r = 2244083/825552 такое, что |exp(1) - r| ≤ 10^-10.

LaTeX

$$$|\exp(1) - \frac{2244083}{825552}| \le 10^{-10}$$$

Lean4

theorem exp_one_near_10 : |exp 1 - 2244083 / 825552| ≤ 1 / 10 ^ 10 :=
  by
  apply exp_approx_start
  iterate 13 refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_
  refine exp_approx_end' _ (by norm_num1; rfl) _ (by norm_cast) (by simp) ?_
  norm_num1

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