[Merged by Bors] - chore: use ‖x‖ₑ instead of ↑‖x‖₊#20806
[Merged by Bors] - chore: use ‖x‖ₑ instead of ↑‖x‖₊#20806YaelDillies wants to merge 1 commit intomasterfrom
‖x‖ₑ instead of ↑‖x‖₊#20806Conversation
PR summary a890aae849Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type |
|---|---|---|
| 4305 | -1 | porting notes |
Current commit a890aae849
Reference commit efeadfb186
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).
grunweg
left a comment
There was a problem hiding this comment.
Three small comments (so far).
|
I pushed a fix for one file; the two others would take me longer. |
|
Thanks for the fix! FYI it's not very useful (to me) to sorry out broken proofs. Sorries (and more generally warnings) aren't picked up in CI until there are no errors left. So sorrying out a proof will make it resurface surprisingly late in the fixing process. |
|
Almost there! For the record, I reviewed every single commit so far and it looks good to me. (I'll try to review the last fixes soon, and then maintainer merge.) |
|
I had to rebase to get rid of the conflict, so I squashed all the commits until fea2a2f. From the second commit onwards are the commits you didn't review, Michael. |
e8ac683 to
c58a9fe
Compare
grunweg
left a comment
There was a problem hiding this comment.
One comment on this commit.
| apply edist_triangle_right | ||
|
|
||
| theorem lintegral_nnnorm_zero : (∫⁻ _ : α, ‖(0 : β)‖₊ ∂μ) = 0 := by simp | ||
| -- Yaël: Why do the following four lemmas even exist? |
There was a problem hiding this comment.
I'm reviewing commit-by-commit: just flagging this so it gets taken care of before merging.
grunweg
left a comment
There was a problem hiding this comment.
I have reviewed everything commit-by-commit now. Thanks a lot for boiling the (mathlib) ocean, Yael!
|
Thanks for the notice! I have reviewed everything up to c58a9fe again. |
8612ff0 to
783ad7b
Compare
|
Squashed everything you've reviewed again |
|
Wait, it builds already? 😱 That's way quicker than I thought! |
|
💪 🐎 🏁 |
|
Should the |
|
!bench |
|
Here are the benchmark results for commit 4bd1ce8. Benchmark Metric Change
===============================================================
- ~Mathlib.MeasureTheory.Function.LpSpace instructions 6.9% |
6 files, Instructions +1.0⬝10⁹
|
I'm pretty sure we could reduce the import increase significantly by splitting Another thing to consider about the present PR is that I needed to add many lemmas about |
|
If you are willing to do that please go ahead! |
4bd1ce8 to
b8947ef
Compare
|
This PR/issue depends on:
|
|
!bench |
|
Here are the benchmark results for commit b8947ef. Benchmark Metric Change
===============================================================
- ~Mathlib.MeasureTheory.Function.LpSpace instructions 6.8% |
2 files, Instructions +1.0⬝10⁹
|
|
I'm a bit surprised by the 10% increase in |
|
I don't have time/know how to investigate, but if someone does so I would be grateful! |
b8947ef to
a890aae
Compare
|
I don't think the tiny slowdown has to keep us from merging this. @grunweg has said he will investigate this later. bors merge |
Rename lemmas from `_nnnorm_`/`_ennnorm_` to `_enorm_` where applicable. Rewrite/golf proofs where necessary.
|
Pull request successfully merged into master. Build succeeded: |
‖x‖ₑ instead of ↑‖x‖₊‖x‖ₑ instead of ↑‖x‖₊
|
See #21179 for the follow-up. |
Rename lemmas from
_nnnorm_/_ennnorm_to_enorm_where applicable. Rewrite/golf proofs where necessary.enorm#20966