gen exp_fun #876
Merged
gen exp_fun #876
Conversation
This file contains hidden or 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
t6s
reviewed
Mar 15, 2023
theories/exp.v
Outdated
| Implicit Types a x : R. | ||
|
|
||
| Definition exp_fun a x := expR (x * ln a). | ||
| Definition power_pos a x := if a == 0 then 0 else expR (x * ln a). |
Member
There was a problem hiding this comment.
Within the current limitation that we cannot properly handle the complex analysis, this definition seems to be the best possible approximation to the power function on R x R. It works for 0 < r < ∞, 0 <= θ < π if seen in the polar coordinate system.
affeldt-aist
added
the
"bug" 🐛
Member
Author
|
@thery Allow me to ping you in case this slipped under your radar |
CohenCyril
added
TODO: MC2 port
proux01
approved these changes
Mar 29, 2023
Collaborator
proux01
left a comment
proux01
left a comment
There was a problem hiding this comment.
Overall looks good to me
Collaborator
|
I'll merge tomorrow if there is no more comment |
- rename to power_pow - fix doc - add scope to notation Co-authored-by: Alessandro Bruni <[email protected]> Co-authored-by: Takafumi Saikawa <[email protected]>
- so that power_pos and exprn coincide
affeldt-aist
force-pushed
the
exp_20230314
branch
from
da01a4b to
bea6c1e
Compare
Member
|
LGTM |
proux01
approved these changes
Mar 31, 2023
Collaborator
proux01
left a comment
proux01
left a comment
There was a problem hiding this comment.
Last changelog comments before I merge
Member
Author
|
Many thanks for the reviews! |
affeldt-aist
added a commit
that referenced
this pull request
Apr 10, 2023
* gen exp_fun - rename to power_pow - fix doc - add scope to notation Co-authored-by: Alessandro Bruni <[email protected]> Co-authored-by: Takafumi Saikawa <[email protected]> * add lemma power12_sqrt * additional lemmas * change power_pos so that 0^0=1 - so that power_pos and exprn coincide * measurable_fun exp ln * fix chaneglog * add power_pos_intmul proposed by Pierre * fix changelog --------- Co-authored-by: Alessandro Bruni <[email protected]> Co-authored-by: Takafumi Saikawa <[email protected]> Co-authored-by: Alessandro Bruni <[email protected]>
proux01
removed
the
TODO: MC2 port
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
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.
Motivation for this change
We @hoheinzollern @t6s needed a bit more general version of
exp_funfor PR #790 and PR #516(in particular to define a power function with extended reals)
Things done/to do
CHANGELOG_UNRELEASED.mdAutomatic note to reviewers
Read this Checklist and put a milestone if possible.