mathlib documentation

data.complex.exponential_bounds

Bounds on specific values of the exponential #

theorem real.exp_one_near_10  :
abs (real.exp 1 - 2244083 / 825552) 1 / 10 ^ 10
theorem real.exp_one_near_20  :
abs (real.exp 1 - 363916618873 / 133877442384) 1 / 10 ^ 20
theorem real.exp_one_gt_d9  :
27182818283 / 10000000000 < real.exp 1
theorem real.exp_one_lt_d9  :
real.exp 1 < 13591409143 / 5000000000
theorem real.exp_neg_one_gt_d9  :
9196986029 / 25000000000 < real.exp (-1)
theorem real.exp_neg_one_lt_d9  :
real.exp (-1) < 919698603 / 2500000000
theorem real.log_two_near_10  :
abs (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