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_271828182  :
135914091 / 50000000 < real.exp 1

theorem real.exp_one_lt_271828183  :
real.exp 1 < 271828183 / 100000000

theorem real.exp_neg_one_gt_0367879441  :
367879441 / 1000000000 < real.exp (-1)

theorem real.exp_neg_one_lt_0367879442  :
real.exp (-1) < 183939721 / 500000000