leanprover-community
feat(Order/Filer/ENNReal): add Real.limsup_mul_le
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
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
![github-actions[bot] avatar](https://avatars.githubusercontent.com/in/15368?v=4 "Published by a pub.dev verified publisher"){kind=small}
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.
Sorry to bother you again, but I'm currently working on proving these lemmas ; I should have a more general version of
limsup_mul_lewith 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.
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.
This PR/issue depends on:
- ~~leanprover-community/mathlib4#18365~~ By Dependent Issues (🤖). Happy coding!
🚀 Pull request has been placed on the maintainer queue by faenuccio.
@urkud Are you happy with the new status of this PR? Do you think we can now let it go?
Please decide without me. I forgot my personal laptop at home, so I won't do anything related to mathlib this week.
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!
🚀 Pull request has been placed on the maintainer queue by faenuccio.
Pull request successfully merged into master.
Build succeeded:
![mathlib-bors[bot] avatar](https://avatars.githubusercontent.com/in/421226?v=4 "Published by a pub.dev verified publisher"){kind=small}