[Merged by Bors] - feat(SpecialFunctions/Log): Add extended exp by LorenzoLuccioli · Pull Request #14107 · leanprover-community/mathlib4

LorenzoLuccioli · 2024-06-24T23:21:26Z

We define an extended version of the exponential from EReal to ENNReal and prove some properties in relation to the extended log.

Rename ENNReal.lean to ENNRealLog.lean
Add ENNRealExp.lean
Add ENNRealLogExp.lean

See this Zulip discussion.

Co-authored-by: @RemyDegenne @pitmonticone @D-Thomine

….github.com> Co-authored-by: Rémy Degenne <Remydegenne@gmail.com>

github-actions · 2024-06-24T23:22:01Z

PR summary f61634fbbc

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Analysis.SpecialFunctions.Log.ENNReal`	-1318
`Mathlib.Analysis.SpecialFunctions.Log.ERealExp`	1064
`Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog`	1316
`Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp`	1354

Declarations diff

+ ENNReal.exp_log
+ EReal.log_exp
+ _root_.EReal.expHomeomorph
+ _root_.EReal.expHomeomorph_apply
+ _root_.EReal.expHomeomorph_symm
+ _root_.EReal.expOrderIso
+ _root_.EReal.expOrderIso_apply
+ _root_.EReal.expOrderIso_symm
+ _root_.EReal.measurable_exp
+ _root_.Measurable.ennreal_log
+ _root_.Measurable.ereal_exp
+ bot_lt_log_iff
+ continuous_exp
+ continuous_log
+ exp
+ exp_add
+ exp_bot
+ exp_coe
+ exp_eq_top_iff
+ exp_eq_zero_iff
+ exp_le_exp_iff
+ exp_le_one_iff
+ exp_lt_exp_iff
+ exp_lt_one_iff
+ exp_lt_top_iff
+ exp_monotone
+ exp_mul
+ exp_neg
+ exp_nmul
+ exp_strictMono
+ exp_top
+ exp_zero
+ instance : PolishSpace ENNReal
+ instance : PolishSpace EReal
+ logHomeomorph
+ logHomeomorph_apply
+ logHomeomorph_symm
+ logOrderIso
+ logOrderIso_apply
+ logOrderIso_symm
+ log_inv
+ log_le_log_iff
+ log_le_zero_iff
+ log_lt_log_iff
+ log_lt_zero_iff
+ log_ofReal
+ log_ofReal_of_pos
+ measurable_log
+ one_le_exp_iff
+ one_lt_exp_iff
+ zero_le_log_iff
+ zero_lt_exp_iff
+ zero_lt_log_iff
- log_bot_lt_iff
- log_continuous
- log_homeomorph
- log_homeomorph_apply
- log_le_iff_le
- log_le_one_iff
- log_lt_iff_lt
- log_lt_one_iff
- log_one_le_iff
- log_one_lt_iff
- log_orderIso
- log_orderIso_apply

You can run this locally as follows

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

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

Co-authored-by: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>

Co-Authored-By: Lorenzo Luccioli <71074618+LorenzoLuccioli@users.noreply.github.com>

Mathlib/Analysis/SpecialFunctions/Log/ENNRealExp.lean

Mathlib/Analysis/SpecialFunctions/Log/ENNRealLogExp.lean

Co-Authored-By: Lorenzo Luccioli <71074618+LorenzoLuccioli@users.noreply.github.com>

pitmonticone · 2024-07-04T13:17:34Z

We should have addressed all the review comments and suggestions.

Thank you very much @sgouezel for your insightful review!

Mathlib/Analysis/SpecialFunctions/Log/ENNRealLogExp.lean

sgouezel

bors d+
Thanks!

Mathlib/Analysis/SpecialFunctions/Log/ENNRealLogExp.lean

mathlib-bors · 2024-07-12T09:04:40Z

✌️ LorenzoLuccioli can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

LorenzoLuccioli · 2024-07-12T12:54:07Z

bors r+

@RemyDegenne

We define an extended version of the exponential from `EReal` to `ENNReal` and prove some properties in relation to the extended log. - [x] Rename `ENNReal.lean` to `ENNRealLog.lean` - [x] Add `ENNRealExp.lean` - [x] Add `ENNRealLogExp.lean` See [this](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Porting.20TopologicalEntropy.20into.20Mathlib/near/446665481) Zulip discussion. Co-authored-by: @RemyDegenne @pitmonticone @D-Thomine Co-authored-by: Lorenzo Luccioli <lorenzoluccioli@gmail.com>

mathlib-bors · 2024-07-12T13:14:47Z

This PR was included in a batch that was canceled, it will be automatically retried

@RemyDegenne

We define an extended version of the exponential from `EReal` to `ENNReal` and prove some properties in relation to the extended log. - [x] Rename `ENNReal.lean` to `ENNRealLog.lean` - [x] Add `ENNRealExp.lean` - [x] Add `ENNRealLogExp.lean` See [this](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Porting.20TopologicalEntropy.20into.20Mathlib/near/446665481) Zulip discussion. Co-authored-by: @RemyDegenne @pitmonticone @D-Thomine Co-authored-by: Lorenzo Luccioli <lorenzoluccioli@gmail.com>

mathlib-bors · 2024-07-12T15:30:41Z

Pull request successfully merged into master.

Build succeeded:

Co-authored-by: Pietro Monticone <38562595+pitmonticone@users.noreply…

0d64f65

….github.com> Co-authored-by: Rémy Degenne <Remydegenne@gmail.com>

LorenzoLuccioli and others added 3 commits June 26, 2024 00:57

Split files, add lemmas

6d5058a

Co-authored-by: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>

Add new files to main

7234098

Co-Authored-By: Lorenzo Luccioli <71074618+LorenzoLuccioli@users.noreply.github.com>

Merge branch 'master' into LL/ERealExp

470e238

pitmonticone mentioned this pull request Jun 27, 2024

Port TopologicalEntropy to Mathlib mseri/BET#64

Merged

LorenzoLuccioli added 4 commits June 30, 2024 01:22

fix lint style

0dd42e4

fix lint

8162c05

fix comments, change theorem to lemma

07607b1

fix comments

5bd0e80

LorenzoLuccioli marked this pull request as ready for review June 29, 2024 23:56

LorenzoLuccioli changed the title ~~feat(SpecialFunctions/Log): Add extended exp~~ feat(SpecialFunctions/Log): Add extended log and exp Jun 30, 2024

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

LorenzoLuccioli changed the title ~~feat(SpecialFunctions/Log): Add extended log and exp~~ feat(SpecialFunctions/Log): Add extended exp Jun 30, 2024

LorenzoLuccioli requested a review from sgouezel June 30, 2024 00:08

LorenzoLuccioli marked this pull request as draft June 30, 2024 00:09

LorenzoLuccioli added 2 commits June 30, 2024 02:19

minimize imports

3854d4c

cleanup

0aa29ec

LorenzoLuccioli marked this pull request as ready for review June 30, 2024 00:22

sgouezel reviewed Jun 30, 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 30, 2024

pitmonticone and others added 7 commits June 30, 2024 16:41

Remove using EReal.rec

b9773da

Co-Authored-By: Lorenzo Luccioli <71074618+LorenzoLuccioli@users.noreply.github.com>

Update ENNRealLogExp.lean

6a11fe5

Co-Authored-By: Lorenzo Luccioli <71074618+LorenzoLuccioli@users.noreply.github.com>

Update ENNRealLogExp.lean

da2a02c

Co-Authored-By: Lorenzo Luccioli <71074618+LorenzoLuccioli@users.noreply.github.com>

Update ENNRealLogExp.lean

819739b

Co-Authored-By: Lorenzo Luccioli <71074618+LorenzoLuccioli@users.noreply.github.com>

Address review comments

c84d9fc

Co-Authored-By: Lorenzo Luccioli <71074618+LorenzoLuccioli@users.noreply.github.com>

add instance for EDist EReal

cda2695

attempt at instance PolishSpace EReal (unfinished)

84f997b

pitmonticone added 2 commits July 4, 2024 15:02

Provisional working state

20070a4

Move PolishSpace instance

051cd13

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

pitmonticone added 2 commits July 4, 2024 15:22

Update ERealExp.lean

8df0538

Update ERealExp.lean

af4b983

sgouezel reviewed Jul 4, 2024

View reviewed changes

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

pitmonticone and others added 2 commits July 5, 2024 01:16

Update ENNRealLogExp.lean

e015003

Add expOrderIso and related lemmas

379df3a

LorenzoLuccioli removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 10, 2024

sgouezel reviewed Jul 10, 2024

View reviewed changes

sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 10, 2024

apply suggestions

086c07b

LorenzoLuccioli removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 10, 2024

sgouezel reviewed Jul 12, 2024

View reviewed changes

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

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jul 12, 2024

Update ENNRealLogExp.lean

f61634f

mathlib-bors bot changed the title ~~feat(SpecialFunctions/Log): Add extended exp~~ [Merged by Bors] - feat(SpecialFunctions/Log): Add extended exp Jul 12, 2024

mathlib-bors bot closed this Jul 12, 2024

mathlib-bors bot deleted the LL/ERealExp branch July 12, 2024 15:30

adomani mentioned this pull request Aug 1, 2024

feat: MiM PR report #15355

Open

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary f61634fbbc

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

pitmonticone commented Jul 4, 2024

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

sgouezel left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mathlib-bors bot commented Jul 12, 2024

Uh oh!

LorenzoLuccioli commented Jul 12, 2024

Uh oh!

mathlib-bors bot commented Jul 12, 2024

Uh oh!

mathlib-bors bot commented Jul 12, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

LorenzoLuccioli commented Jun 24, 2024 •

edited

Loading

github-actions bot commented Jun 24, 2024 •

edited

Loading