Commit 2021-08-26 07:01 cb1932d7

feat(data/complex/exponential): bound on exp for arbitrary arguments (#8667) This PR is for a new lemma (currently called exp_bound') which proves exp x is close to its nth degree taylor expansion for sufficiently large n. Unlike the previous bound, this lemma can be instantiated on any real x rather than just x with absolute value less than or equal to 1. I am separating this lemma out from #8002 because I think it stands on its own. The last time I checked it was sorry free - but that was before I merged with master and moved it to a different branch. It may also benefit from a little golfing. There are a few lemmas I proved as well to support this - one about the relative size of factorials and a few about sums of geometric sequences. The geometric series ones should probably be generalized and moved to another file this generalization sort of exists and is in the algebra.geom_sum file. I didn't find it initially since I was searching for "geometric" not "geom".