Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-19 10:38 47dcecd2

View on Github →

feat(data/complex/exponential): bounds on exp (#4432) Define real.exp_bound using complex.exp_bound. Deduce numerical bounds on exp 1 analogous to those we have for pi.

Estimated changes

Modified src/data/complex/exponential.lean

added theorem real.exp_1_approx_succ_eq

added theorem real.exp_approx_end'

added theorem real.exp_approx_end

added theorem real.exp_approx_start

added theorem real.exp_approx_succ

added theorem real.exp_bound

added def real.exp_near

added theorem real.exp_near_sub

added theorem real.exp_near_succ

added theorem real.exp_near_zero

Created src/data/complex/exponential_bounds.lean

added theorem real.exp_neg_one_gt_0367879441

added theorem real.exp_neg_one_lt_0367879442

added theorem real.exp_one_gt_271828182

added theorem real.exp_one_lt_271828183

added theorem real.exp_one_near_10

added theorem real.exp_one_near_20