Conversation
|
I can try to help with the variables/types. Do you have a particular question? |
|
Looking at the diff, it seems that your change was based on an older version of this file, as it reverts a recent PR. I could re-apply the old PR, for instance - if that is helpful for you. |
I changed some types (changed NormedSpace to MulActionWithZero + IsBoundedSMul) to generalize most of the results, and then added NormedSpace only before a couple lemmas that needed them. There is a linter warning that I don't fully understand, probably should be fixed reorganizing the sections and variable declarations. |
I don't fully understand (this is my first PR ever), but I guess this is helpful, yes. |
|
I pushed some changes which seemed fine; there are probably a few more... but for that, I need to look at your PR locally. I'm working on that, but setting this up takes a while. I'm out of Lean time for today, but can hopefully return to this on Monday. |
|
Sorry for the delay: my computer broke and I was travelling. Applying your PR against the latest version of the project, there are now build failures. Would you like to look into them? (I can also do it.) |
grunweg
left a comment
grunweg
left a comment
There was a problem hiding this comment.
Playing with your file locally, I found a fix for the variables issue. I'll create a PR with my changes on top of yours tonight, so you can take a look yourself.
I also gave the new lemmas a brief review for coding style: this is what I would say on a mathlib PR. (For this PR, you need not address all of these, but I figured you may find this helpful to know anyway.)
| lemma wnorm_const_smul_le {𝕜 E α : Type*} [NormedAddCommGroup E] {_x : MeasurableSpace α} | ||
| {p : ℝ≥0∞} (hp : p ≠ 0) {μ : Measure α} {f : α → E} | ||
| [NontriviallyNormedField 𝕜] [MulActionWithZero 𝕜 E] [IsBoundedSMul 𝕜 E] (k : 𝕜) : | ||
| wnorm (k • f) p μ ≤ ‖k‖₊ * wnorm f p μ := by |
There was a problem hiding this comment.
Mathlib style is to always indent the proofs by two spaces. You use four-space indent for subsequent lines of theorem statements.
| {p : ℝ≥0∞} (hp : p ≠ 0) {μ : Measure α} {f : α → E} | ||
| [NontriviallyNormedField 𝕜] [MulActionWithZero 𝕜 E] [IsBoundedSMul 𝕜 E] (k : 𝕜) : | ||
| wnorm (k • f) p μ ≤ ‖k‖₊ * wnorm f p μ := by | ||
| unfold wnorm |
There was a problem hiding this comment.
I'd move this into the simp, making that simp [wnorm, ptop, wnorm'].
| intro f hf | ||
| refine ⟨aestronglyMeasurable_const.smul (h f hf).1, ?_⟩ | ||
| sorry | ||
| calc |
There was a problem hiding this comment.
I'd indent this slightly more compactly, as
calc wnorm ((k • T) f) p' ν
_ ≤ ↑‖k‖₊ * wnorm (T f) p' ν := by simp [wnorm_const_smul_le hp']
_ ≤ ↑‖k‖₊ * (c * eLpNorm f p μ) := by
gcongr
apply (h f hf).2
_ = ↑(‖k‖₊ * c) * eLpNorm f p μ := by simp [coe_mul, mul_assoc]
In fact, you can use the enorm for many steps, which might be even nicer:
calc wnorm ((k • T) f) p' ν
_ ≤ ‖k‖ₑ * wnorm (T f) p' ν := by simp [wnorm_const_smul_le hp']
_ ≤ ‖k‖ₑ * (c * eLpNorm f p μ) := by
gcongr
apply (h f hf).2
_ = (‖k‖ₑ * c) * eLpNorm f p μ := by simp [coe_mul, mul_assoc]
|
#281 contains most of the clean-ups I would make: the build fails in the proof of |
|
Since I'm actively working on this file and this PR ought to go in first, let me go ahead and merge this PR. I'll push #281 immediately afterwards, which should fix the build. (If the one intermediate commit is an issue, I'm happy to force-push history later.) |
|
Thanks for your PR! |
Clean-ups on top of #275: remove unintentional changes, align style more with mathlib and clean up the variable blocks. Now, each theorem only asks for the minimal necessary typeclass assumptions, and it is clear which theorems require normed spaces and which ones don't. All in all, #275 and this PR together - correct the statement of HasWeakType.const_mul (which only holds for `p' ≠ 0`) - completes the proof of `HasWeakType.const_mul` - weaken the hypotheses in this file: many lemmas only require `[MulActionWithZero 𝕜 E] [IsBoundedSMul 𝕜 E]` and not `[NormedSpace 𝕜 E]`
2 participants
Proved lemmas:
lemma HasWeakType.const_mul
lemma HasWeakType.const_smul
Created and proved lemma:
lemma wnorm_const_smul_le
Messed up some variables / types, needs help