[Merged by Bors] - feat(SpecialFunctions/Log): add extended nonnegative real logarithm by pitmonticone · Pull Request #14018 · leanprover-community/mathlib4

pitmonticone · 2024-06-21T15:29:18Z

This PR adds the SpecialFunctions/Log/ENNRealLog.lean file where we define log as an extension of the logarithm of a positive real to the extended nonnegative reals ℝ≥0∞. The function takes values in the extended reals EReal, with log 0 = ⊥ and log ⊤ = ⊤.

Co-authored with @D-Thomine.

Co-Authored-By: D-Thomine <100795491+D-Thomine@users.noreply.github.com>

github-actions · 2024-06-21T15:29:52Z

PR summary 269142b3fb

Import changes

No significant changes to the import graph

Declarations diff

+ log
+ log_bijective
+ log_bot_lt_iff
+ log_continuous
+ log_eq_bot_iff
+ log_eq_iff
+ log_eq_one_iff
+ log_eq_top_iff
+ log_homeomorph
+ log_homeomorph_apply
+ log_injective
+ log_le_iff_le
+ log_le_one_iff
+ log_lt_iff_lt
+ log_lt_one_iff
+ log_lt_top_iff
+ log_monotone
+ log_mul_add
+ log_of_nnreal
+ log_one
+ log_one_le_iff
+ log_one_lt_iff
+ log_orderIso
+ log_orderIso_apply
+ log_pos_real
+ log_pos_real'
+ log_pow
+ log_rpow
+ log_strictMono
+ log_surjective
+ log_top
+ log_zero

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

Co-Authored-By: D-Thomine <100795491+D-Thomine@users.noreply.github.com>

sgouezel

Are you planning to also add exp in the other direction? (I'm asking because the order iso version and the homeomorphism version would love to have a simp lemma saying that, when you apply their symm, it coincides with exp). If yes in a near future, then everything is perfect. If not, can you add a todo about this at the end of the file-level comment?

Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean

dupuisf

I just have a few comments, but globally it looks good! I think it would be good to also add lemmas about (ENNReal.log x).toReal, my guess is that it would come up in practice quite a bit.

Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean

dupuisf · 2024-06-21T20:08:31Z

(Sorry about some of the double comments, I was reviewing at the same time as Sébastien...)

pitmonticone · 2024-06-22T01:05:00Z

Are you planning to also add exp in the other direction? (I'm asking because the order iso version and the homeomorphism version would love to have a simp lemma saying that, when you apply their symm, it coincides with exp). If yes in a near future, then everything is perfect. If not, can you add a todo about this at the end of the file-level comment?

No, unfortunately I won't have enough time in the near future. I'm going to add the TODO.

pitmonticone · 2024-06-22T01:12:03Z

Ok, I should have addressed all the review requests.

Thank you very much @sgouezel and @dupuisf for your quick and insightful reviews!

Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>

Mathlib/Analysis/SpecialFunctions/Log/ENNReal.lean

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

pitmonticone · 2024-06-22T13:50:11Z

I should have addressed all the review requests.

Thank you very much @sgouezel and @dupuisf for your reviews!

pitmonticone · 2024-06-23T14:35:30Z

Now I should have really addressed all the review requests 😅.

Thank you again @sgouezel and @dupuisf for your reviews!

sgouezel · 2024-06-23T16:18:46Z

bors r+
Thanks!

@D-Thomine

…14018) This PR adds the `SpecialFunctions/Log/ENNRealLog.lean` file where we define `log` as an extension of the logarithm of a positive real to the extended nonnegative reals `ℝ≥0∞`. The function takes values in the extended reals `EReal`, with `log 0 = ⊥` and `log ⊤ = ⊤`. Co-authored with @D-Thomine.

mathlib-bors · 2024-06-23T16:28:53Z

Pull request successfully merged into master.

Build succeeded:

@D-Thomine

…14018) This PR adds the `SpecialFunctions/Log/ENNRealLog.lean` file where we define `log` as an extension of the logarithm of a positive real to the extended nonnegative reals `ℝ≥0∞`. The function takes values in the extended reals `EReal`, with `log 0 = ⊥` and `log ⊤ = ⊤`. Co-authored with @D-Thomine.

@D-Thomine

…14018) This PR adds the `SpecialFunctions/Log/ENNRealLog.lean` file where we define `log` as an extension of the logarithm of a positive real to the extended nonnegative reals `ℝ≥0∞`. The function takes values in the extended reals `EReal`, with `log 0 = ⊥` and `log ⊤ = ⊤`. Co-authored with @D-Thomine.

feat(SpecialFunctions/Log): add extended nonnegative real logarithm

66c8649

Co-Authored-By: D-Thomine <100795491+D-Thomine@users.noreply.github.com>

pitmonticone added awaiting-review t-analysis Analysis (normed *, calculus) labels Jun 21, 2024

pitmonticone and others added 2 commits June 21, 2024 17:34

Update ENNRealLog.lean

59a4c32

Co-Authored-By: D-Thomine <100795491+D-Thomine@users.noreply.github.com>

Update ENNRealLog.lean

41a1ae4

Co-Authored-By: D-Thomine <100795491+D-Thomine@users.noreply.github.com>

pitmonticone marked this pull request as ready for review June 21, 2024 15:41

pitmonticone requested a review from sgouezel June 21, 2024 15:46

Update Mathlib.lean

fa7ada1

sgouezel reviewed Jun 21, 2024

View reviewed changes

sgouezel added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jun 21, 2024

dupuisf reviewed Jun 21, 2024

View reviewed changes

Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean Outdated Show resolved Hide resolved

Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean Outdated Show resolved Hide resolved

pitmonticone added 11 commits June 21, 2024 22:09

Rename file

4f7db74

Update module doc

dd12c45

Update ENNReal.lean

e18bb8b

Update ENNReal.lean

593f8f8

Update ENNReal.lean

aad60d6

Update ENNReal.lean

3d76b89

Update ENNReal.lean

c3bc1f0

Update ENNReal.lean

be534e1

Update ENNReal.lean

c0268b1

Update ENNReal.lean

b573314

Update ENNReal.lean

da4a580

pitmonticone added 2 commits June 22, 2024 03:07

Update ENNReal.lean

54b4271

Update ENNReal.lean

51abf63

pitmonticone removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 22, 2024

Update ENNReal.lean

6d75fe5

Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>

sgouezel reviewed Jun 22, 2024

View reviewed changes

sgouezel added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jun 22, 2024

pitmonticone and others added 4 commits June 22, 2024 15:20

Update Mathlib/Analysis/SpecialFunctions/Log/ENNReal.lean

2e3c967

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Update ENNReal.lean

d5138ad

Update ENNReal.lean

ab282fa

Update ENNReal.lean

0f30737

pitmonticone added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 22, 2024

pitmonticone requested review from dupuisf and sgouezel June 22, 2024 13:33

sgouezel added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jun 23, 2024

Update ENNReal.lean

269142b

pitmonticone added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 23, 2024

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 23, 2024

mathlib-bors bot changed the title ~~feat(SpecialFunctions/Log): add extended nonnegative real logarithm~~ [Merged by Bors] - feat(SpecialFunctions/Log): add extended nonnegative real logarithm Jun 23, 2024

mathlib-bors bot closed this Jun 23, 2024

mathlib-bors bot deleted the pitmonticone/ENNRealLog branch June 23, 2024 16:28

pitmonticone mentioned this pull request Jun 27, 2024

Port TopologicalEntropy to Mathlib mseri/BET#64

Merged

Conversation

pitmonticone commented Jun 21, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jun 21, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 269142b3fb

Import changes

Declarations diff

Uh oh!

sgouezel left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

dupuisf left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

dupuisf commented Jun 21, 2024

Uh oh!

pitmonticone commented Jun 22, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

pitmonticone commented Jun 22, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

pitmonticone commented Jun 22, 2024

Uh oh!

pitmonticone commented Jun 23, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sgouezel commented Jun 23, 2024

Uh oh!

mathlib-bors bot commented Jun 23, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

pitmonticone commented Jun 21, 2024 •

edited

Loading

github-actions bot commented Jun 21, 2024 •

edited

Loading

pitmonticone commented Jun 22, 2024 •

edited

Loading

pitmonticone commented Jun 22, 2024 •

edited

Loading

pitmonticone commented Jun 23, 2024 •

edited

Loading