[Merged by Bors] - feat(Algebra/Order/Ring/Unbundled/Nonneg.lean): add boundedness lemmas by mariainesdff · Pull Request #18172 · leanprover-community/mathlib4

mariainesdff · 2024-10-24T13:33:33Z

Lemmas about limsup and bddAbove needed for #15373.

depends on: [Merged by Bors] - feat: liminf and limsup add/mul lemmas in Real #18365

github-actions · 2024-10-24T13:34:24Z

PR summary 38a8f125e3

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ BddAbove.range_comp_of_nonneg
+ MonotoneOn.mul
+ bddAbove_range_mul
+ eventually_add_neg_lt_of_le_liminf
+ eventually_lt_add_pos_of_limsup_le
+ exists_lt_of_le_liminf
+ exists_lt_of_limsup_le

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>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

D-Thomine · 2024-10-24T20:26:44Z

Sorry to bother you again, but I'm currently working on proving these lemmas ; I should have a more general version of limsup_mul_le with a much shorter proof (and many more similar lemmas). Would you mind waiting for a few days?

Is there anything you need for your project beyond limsup_mul_le? The coe lemmas look interesting.

mariainesdff · 2024-10-25T15:54:36Z

Sorry to bother you again, but I'm currently working on proving these lemmas ; I should have a more general version of limsup_mul_le with a much shorter proof (and many more similar lemmas). Would you mind waiting for a few days?

Is there anything you need for your project beyond limsup_mul_le? The coe lemmas look interesting.

When do you think you will have it ready?

These are all used in #15373. The coercion lemmas are only used in the proof of Real.limsup_le (so if you have a better proof, I probably will not need them), but the remaining lemmas are used in the file Analysis/Normed/Ring/SmoothingSeminorm in that PR, so I need to keep them.

Ruben-VandeVelde · 2024-10-26T08:28:21Z

Please remove the label again on Monday if no news

D-Thomine · 2024-10-29T13:36:06Z

A more general version of limsup_mul_le is in #18365 (arbitrary filters, and the nonnegativity/boundedness conditions are replaced by appropriate eventual/frequent properties). Your own version should follow quite quickly from it.

mathlib4-dependent-issues-bot · 2024-11-01T12:04:33Z

This PR/issue depends on:

~~[Merged by Bors] - feat: liminf and limsup add/mul lemmas in Real #18365~~
By Dependent Issues (🤖). Happy coding!

Mathlib/Data/Real/Basic.lean

Mathlib/Topology/EMetricSpace/Basic.lean

Mathlib/Topology/Instances/ENNReal.lean

Mathlib/Topology/EMetricSpace/Basic.lean

faenuccio

Thanks, modulo a couple of golfing comments it LGTM.

Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

faenuccio · 2024-12-18T15:32:26Z

Thanks!

faenuccio · 2024-12-18T15:32:31Z

maintainer merge

github-actions · 2024-12-18T15:32:50Z

🚀 Pull request has been placed on the maintainer queue by faenuccio.

Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

Mathlib/Order/Filter/ENNReal.lean

urkud · 2024-12-20T05:20:33Z

Mathlib/Algebra/Order/Ring/Unbundled/Nonneg.lean

+/-- If `u v : α → β` are nonnegative and bounded above, then `u * v` is bounded above. -/
+theorem bddAbove_range_mul {α β : Type*} {u v : α → β} [Preorder β] [Zero β] [Mul β] [PosMulMono β]
+    [MulPosMono β] (hu : BddAbove (Set.range u)) (hu0 : 0 ≤ u)
+    (hv : BddAbove (Set.range v)) (hv0 : 0 ≤ v) : BddAbove (Set.range (u * v)) := by


Please golf using BddAbove.range_comp

I don't see how that is possible without adding extra hypotheses, so I have added a new version BddAbove.range_comp_of_nonneg and used it to golf the proof.

Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

urkud · 2024-12-20T05:23:14Z

Also, please fix the title: the PR doesn't modify EMetricSpace/*.

faenuccio · 2025-01-13T09:41:25Z

@urkud Are you happy with the new status of this PR? Do you think we can now let it go?

urkud · 2025-01-13T09:59:10Z

Please decide without me. I forgot my personal laptop at home, so I won't do anything related to mathlib this week.

faenuccio · 2025-01-13T10:30:19Z

Please decide without me. I forgot my personal laptop at home, so I won't do anything related to mathlib this week.

OK, then I think I will go ahead. Thanks!

faenuccio · 2025-01-13T10:30:24Z

maintainer merge

github-actions · 2025-01-13T10:30:45Z

🚀 Pull request has been placed on the maintainer queue by faenuccio.

jcommelin

Thanks 🎉

bors merge

#18172) Lemmas about limsup and bddAbove needed for #15373. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

mathlib-bors · 2025-01-13T15:52:01Z

Pull request successfully merged into master.

Build succeeded:

feat(Order/Filer/ENNReal): add Real.limsup_mul_le

7396ff9

mariainesdff added the t-analysis Analysis (normed *, calculus) label Oct 24, 2024

mariainesdff mentioned this pull request Oct 24, 2024

[Merged by Bors] - feat(Analysis.Normed.Ring.Seminorm): add SmoothingSeminorm #15373

Closed

6 tasks

Ruben-VandeVelde added the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 26, 2024

mariainesdff removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 28, 2024

D-Thomine mentioned this pull request Oct 29, 2024

[Merged by Bors] - feat: liminf and limsup add/mul lemmas in Real #18365

Closed

mathlib4-dependent-issues-bot added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Oct 30, 2024

mariainesdff added the WIP Work in progress label Nov 4, 2024

mariainesdff added 4 commits November 4, 2024 10:24

Merge branch 'master' into mariainesdff/limsup

c437fb8

Merge branch 'master' into mariainesdff/limsup

612de46

apply lemma

dbb77f9

delete lemmas

ea8032b

mariainesdff changed the title ~~feat(Order/Filer/ENNReal): add Real.limsup_mul_le~~ feat(Topology/EMetricSpace/Basic): add boundedness lemmas Nov 11, 2024

mariainesdff removed the WIP Work in progress label Nov 11, 2024

j-loreaux reviewed Nov 13, 2024

View reviewed changes

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 13, 2024

mariainesdff added 3 commits November 21, 2024 11:32

partial review changes

c1b3da5

remaining suggested changes

aa98326

Merge branch 'master' into mariainesdff/limsup

c10d77b

mariainesdff removed the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 21, 2024

faenuccio reviewed Dec 11, 2024

View reviewed changes

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 16, 2024

suggested changes

9708127

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Dec 18, 2024

urkud reviewed Dec 20, 2024

View reviewed changes

Mathlib/Topology/Algebra/Order/LiminfLimsup.lean Outdated Show resolved Hide resolved

Update Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

e12ba3b

urkud reviewed Dec 20, 2024

View reviewed changes

Mathlib/Order/Filter/ENNReal.lean Show resolved Hide resolved

urkud reviewed Dec 20, 2024

View reviewed changes

Mathlib/Topology/Algebra/Order/LiminfLimsup.lean Outdated Show resolved Hide resolved

urkud added awaiting-author A reviewer has asked the author a question or requested changes. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Dec 20, 2024

suggested changes

57f77c7

mariainesdff changed the title ~~feat(Topology/EMetricSpace/Basic): add boundedness lemmas~~ feat( Algebra/Order/Ring/Unbundled/Nonneg.lean): add boundedness lemmas Jan 7, 2025

Merge branch 'master' into mariainesdff/limsup

38a8f12

mariainesdff removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 7, 2025

mariainesdff changed the title ~~feat( Algebra/Order/Ring/Unbundled/Nonneg.lean): add boundedness lemmas~~ feat(Algebra/Order/Ring/Unbundled/Nonneg.lean): add boundedness lemmas Jan 7, 2025

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 13, 2025

jcommelin reviewed Jan 13, 2025

View reviewed changes

ghost added the ready-to-merge This PR has been sent to bors. label Jan 13, 2025

mathlib-bors bot pushed a commit that referenced this pull request Jan 13, 2025

feat(Algebra/Order/Ring/Unbundled/Nonneg.lean): add boundedness lemmas (

e9171f0

#18172) Lemmas about limsup and bddAbove needed for #15373. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

mathlib-bors bot changed the title ~~feat(Algebra/Order/Ring/Unbundled/Nonneg.lean): add boundedness lemmas~~ [Merged by Bors] - feat(Algebra/Order/Ring/Unbundled/Nonneg.lean): add boundedness lemmas Jan 13, 2025

mathlib-bors bot closed this Jan 13, 2025

mathlib-bors bot deleted the mariainesdff/limsup branch January 13, 2025 15:52

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary 38a8f125e3

Import changes for modified files

Declarations diff

Uh oh!

D-Thomine commented Oct 24, 2024

Uh oh!

mariainesdff commented Oct 25, 2024

Uh oh!

Ruben-VandeVelde commented Oct 26, 2024

Uh oh!

D-Thomine commented Oct 29, 2024

Uh oh!

mathlib4-dependent-issues-bot commented Nov 1, 2024

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

faenuccio left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

faenuccio commented Dec 18, 2024

Uh oh!

faenuccio commented Dec 18, 2024

Uh oh!

github-actions bot commented Dec 18, 2024

Uh oh!

Uh oh!

Uh oh!

urkud Dec 20, 2024

Choose a reason for hiding this comment

Uh oh!

mariainesdff Jan 7, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

urkud commented Dec 20, 2024

Uh oh!

faenuccio commented Jan 13, 2025

Uh oh!

urkud commented Jan 13, 2025

Uh oh!

faenuccio commented Jan 13, 2025

Uh oh!

faenuccio commented Jan 13, 2025

Uh oh!

github-actions bot commented Jan 13, 2025

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jan 13, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants

mariainesdff commented Oct 24, 2024 •

edited

Loading

github-actions bot commented Oct 24, 2024 •

edited

Loading