feat: bump to 4.16.0rc2 #206
Conversation
There was a problem hiding this comment.
Thanks a lot for your PR! Looks good to me, just three small comments.
@fpvandoorn maintainer merge (i.e., you may want to take a look)
| @@ -1,4 +1,4 @@ | |||
| import Carleson.ToMathlib.Analysis.SumIntegralComparisons | |||
| import Mathlib.Analysis.SumIntegralComparisons | |||
| import Mathlib.Analysis.SpecialFunctions.Integrals | |||
There was a problem hiding this comment.
Should this file move to ToMathlib? (Are there are sorries left? I didn't check.)
If so, can you add a TODO comment (no need to move now)?
There was a problem hiding this comment.
It looks a little bit too specialized to me for mathlib.
| @@ -285,13 +285,13 @@ lemma adjoint_tree_estimate (hu : u ∈ t) (hf : BoundedCompactSupport f) : | |||
| eLpNorm (adjointCarlesonSum (t u) f) 2 volume ≤ | |||
| C7_4_2 a * dens₁ (t u) ^ (2 : ℝ)⁻¹ * eLpNorm f 2 volume := by | |||
| rw [C7_4_2_def] | |||
| let g := adjointCarlesonSum (t u) f | |||
| set g := adjointCarlesonSum (t u) f with h'g | |||
There was a problem hiding this comment.
This is not needed, right?
There was a problem hiding this comment.
The set instead of let is necessary, but the with clause is not so I've removed it.
Carleson/RealInterpolation.lean
Outdated
| @@ -2486,7 +2486,7 @@ lemma estimate_trnc {p₀ q₀ q : ℝ} {spf : ScaledPowerFunction} {j : Bool} | |||
| (p₀⁻¹ * q₀) := by | |||
| have := spf.hd | |||
| unfold eLpNorm eLpNorm' | |||
| let tc := spf_to_tc spf | |||
| set tc := spf_to_tc spf with htc | |||
There was a problem hiding this comment.
Again, the set is necessary, but the with clause is not so I've removed it.
|
Thanks! I'm just going to hope there is no semantic merge conflict with the previous just-merged PR. |
|
Oh that was a mistake. If someone can fix the build, that would be great. |
|
I'll fix it. |
|
Fix at #207 |
I've upstreamed several things already, so this makes for a nice cleanup.