[Merged by Bors] - feat(data/complex/exponential): bound on exp for arbitrary arguments #8667
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Closed
11 tasks
ericrbg
reviewed
Aug 15, 2021
Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com>
BoltonBailey
added
awaiting-review
semorrison
changed the title
eric-wieser
reviewed
Aug 16, 2021
semorrison
reviewed
Aug 16, 2021
semorrison
reviewed
Aug 16, 2021
|
Would it be possible to use a lemma characterising |
eric-wieser
reviewed
Aug 16, 2021
sgouezel
removed
the
awaiting-review
BoltonBailey
added
awaiting-review
|
If #8576 is coming in the next few days, and you all think it's important to avoid changing this until it's done feel free to block this. Otherwise, I can also address any other comments about the code. |
bryangingechen
changed the title
jcommelin
reviewed
Aug 18, 2021
jcommelin
added
awaiting-author
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Johan Commelin <johan@commelin.net>
BoltonBailey
added
awaiting-review
|
I pushed a golf. |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Aug 26, 2021
…8667) This PR is for a new lemma (currently called `exp_bound'`) which proves `exp x` is close to its `n`th 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".
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR is for a new lemma (currently called
exp_bound') which provesexp xis close to itsnth degree taylor expansion for sufficiently largen. Unlike the previous bound, this lemma can be instantiated on any realxrather than justxwith 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 filethis 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".