Bounds on specific values of the exponential #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem real.exp_one_near_10 :

|rexp 1 - 2244083 / 825552| ≤ 1 / 10 ^ 10

theorem real.exp_one_near_20 :

|rexp 1 - 363916618873 / 133877442384| ≤ 1 / 10 ^ 20

theorem real.exp_one_gt_d9 :

27182818283 / 10000000000 < rexp 1

theorem real.exp_one_lt_d9 :

rexp 1 < 13591409143 / 5000000000

9196986029 / 25000000000 < rexp (-1)

rexp (-1) < 919698603 / 2500000000

theorem real.log_two_near_10 :

|real.log 2 - 287209 / 414355| ≤ 1 / 10 ^ 10

theorem real.log_two_gt_d9 :

6931471803 / 10000000000 < real.log 2

theorem real.log_two_lt_d9 :

real.log 2 < 108304247 / 156250000