jmmarulang

natural logarithm for the extended reals and some simple lemmas

2

##### Motivation for this change the natural logarithm for the extended reals is needed for extending hoelder into the extended reals. ##### Checklist - [X] added corresponding entries in `CHANGELOG_UNRELEASED.md`...

PoweR with extended real exponents

4

##### Motivation for this change ##### Checklist - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [ ] added corresponding documentation in the headers Reference: [How to document](https://github.com/math-comp/math-comp/wiki/How-to-document) ##### Merge...

Should poweR return 0 if the exponent is negative?

1

See the following definition https://github.com/math-comp/analysis/blob/97d07798ab1fd1889ed707181c06cf98c438e408/theories/exp.v#L996-L1001 Note that for real numbers, the limit of the power function when the exponent is negative, goes to 0.