[Merged by Bors] - feat: generalize measure-theoretic definitions using ENorm#20122
[Merged by Bors] - feat: generalize measure-theoretic definitions using ENorm#20122fpvandoorn wants to merge 20 commits intomasterfrom
Conversation
PR summary 7b7a268b60Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
|
This PR/issue depends on:
|
grunweg
left a comment
There was a problem hiding this comment.
I know this is WIP PR; I took a look anyway. I only have small comments. My biggest two are
- would a separate PR for the two small golfs make sense (optional)
- I wonder if splitting the rename
Enorm->ENormedSpaceinto a separate PR makes sense (I'll happily approve, I'll be online occasionally until the 26th) - should that rename have a deprecation?
| /-- Auxiliary class, endowing a type `α` with a function `enorm : α → ℝ≥0∞` with notation `‖x‖ₑ`. -/ | ||
| @[notation_class] | ||
| class ENorm (E : Type*) where | ||
| /-- the `ℝ≥0∞`-valued norm function. -/ |
There was a problem hiding this comment.
| /-- the `ℝ≥0∞`-valued norm function. -/ | |
| /-- the `ℝ≥0∞`-valued norm function -/ |
|
Update: never mind, most of diff was from a dependent PR. That answers my questions about deprecations, splitting a rename etc. |
|
I don't think I'll spend time on finishing this in the next few days. Feel free to fix the remaining broken proofs if you have time. |
| simp_rw [inner_def, ← integral_add (integrable_inner f g) (integrable_inner f' g), ← | ||
| inner_add_left] | ||
| simp_rw [inner_def] | ||
| rw [← integral_add (integrable_inner f g) (integrable_inner f' g)] |
There was a problem hiding this comment.
I'm not quite sure why this change is necessary. (Making everything one simp_rw certainly fails now.)
A careful look if there are deeper issues would be appreciated.
There was a problem hiding this comment.
It unfolded the definition of HasFiniteIntegral. I added hasFiniteIntegral_iff_nnnorm.
There was a problem hiding this comment.
Never mind, that was elsewhere.
There is nothing in the conclusion of integrable_inner that identifies 𝕜.
It probably should be explicit, and I assume that before it could be synthesized using simple unification of instance arguments, which now fails.
There was a problem hiding this comment.
Thanks for the clarification! I agree with your fixes.
I'll put "make k in integrable_inner explicit" on my follow-up list of PR - in the new year.
|
@fpvandoorn mathlib CI passes now. Double-checking some changes could be helpful (I've commented on them); most fixes were indeed uncontroversial. |
|
Thanks for finishing the fixes. It is now ready to merge on my side |
|
From my side, this PR is also good to go. I cannot approve my own changes, of course, but since I'm not a maintainer anyway, let me |
|
🚀 Pull request has been placed on the maintainer queue by grunweg. |
* Lemmas are *not* generalized yet (some lemmas can be generalized by just weakening the typeclasses, but others require rules how `enorm` interacts with algebraic operations). * All proofs that broke unfolded the definition. Now they rewrite with a lemma giving the definition in terms of `nnnorm`. Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
|
Pull request successfully merged into master. Build succeeded: |
It was broken in #20122. From GibbsMeasure
Extracted from #21375: these lemmas only change the assumption on the co-domain, but not any hypothesis. This continues the work started in #20121, #20122 and #21306: those PRs generalised the definitions resp. made lemma statements use the enorm. This PR starts generalising the lemmas using those definitions. This work is part of (and a necessary pre-requisite for) the Carleson project.
Extracted from #21375: these lemmas only change the assumption on the co-domain, but not any hypothesis. This continues the work started in #20121, #20122 and #21306: those PRs generalised the definitions resp. made lemma statements use the enorm. This PR starts generalising the lemmas using those definitions. This work is part of (and a necessary pre-requisite for) the Carleson project.
enorminteracts with algebraic operations).nnnorm.