Outstanding Tasks, V6

Stream: Carleson

[Floris van Doorn]

It's time for a new list of tasks!

Below are the remaining tasks, filtering the completed tasks from the last post. I added tasks for chapter 3, and the remaining tasks for chapter 6 (feel free to claim the two that Maria hasn't worked on yet). Hopefully these are all the tasks needed to finish the project!

There is a CONTRIBUTING file with some useful tips.

Tasks:

82 :check: (Michael Rothgang) Prove Lemma 7.4.4
83 :check: (Jeremy Tan) Prove Lemma 7.4.5
84 :check: (Jeremy Tan) Prove Lemma 7.4.6
98 :check: (Jeremy Tan) Prove Lemma 7.6.2
102 :play: (Edward van de Meent) Prove Lemma 7.7.2
103 :check: (Jeremy Tan) Prove Lemma 7.7.3
105 :check: (Jeremy Tan) Prove Proposition 2.0.4

For the next tasks see this thread for more information.

113 :check: (Michael Rothgang, mostly done) Upstream https://florisvandoorn.com/carleson/docs/Carleson/ToMathlib/ENorm.html (we might need to discuss if we're happy with these exact classes)
114 :check: (Michael Rothgang, mostly done) Generalize all Mathlib lemmas that can be generalized to one of the classes in 113 to the appropriate class. (depends on 113)
116 :check: (Michael Rothgang, Jim Portegies, Leo Diedering, Jeremy Tan) Generalize the proof of the real interpolation theorem to also include operators mapping into ENNReal A start of this has been made in #209 (depends partly on 114, 115)
117 :check: (Michael Rothgang, Jim Portegies, Jeremy Tan) Fix all sorry's introduced in 111 by translating all the proof so that they use ENNReal directly. (depends on 115, 116) (We will mark Proposition 2.0.6 as completed once this is finished)

124 :check: (Jasper Mulder-Sohn) Prove Lemma 10.1.6
125 :check: (Jasper Mulder-Sohn) Prove Lemma 10.1.7
126 :check: (Jasper Mulder-Sohn) Prove Lemma 10.1.8
127 :check: (Jasper Mulder-Sohn, Jim Portegies) Prove Lemma 10.0.2

128 :check: (James Sundstrom) Prove Lemma 11.3.1
130 :check: (Dennis Tsar) Prove Lemma 11.3.4
131 :check: (Sébastien Gouëzel) Prove Lemma 11.3.5
132 :check: (Sébastien Gouëzel) Prove Lemma 11.1.6 (hard)

136 :check: (James Sundstrom) Prove Lemma 10.2.2
137 :check: (Jeremy Tan) Prove Lemma 10.2.4
138 :check: (James Sundstrom and a bit by Dennis Tsar) Prove Lemma 10.2.5. This lemma has a long statement and proof. I already formalized a skeleton of the proof, and this now consists of 21 sorry'd statements in the section "Lemma 10.2.5", most of which are pretty easy. Feel free to claim only part of these sorry's.
139 :check: (James Sundstrom) Prove Lemma 10.2.6
140 :check: (James Sundstrom) Prove Lemma 10.2.7 (long)
141 :check: (Jeremy Tan) Prove Lemma 10.2.8
142 :check: (Jeremy Tan) Prove Lemma 10.2.9
143 :check: (Jeremy Tan) Prove Lemma 10.0.3
144 :check: (James Sundstrom) Prove Theorem 10.0.1

145 :check: (María Inés de Frutos Fernández) Prove Lemma 6.3.4
146 :check: (María Inés de Frutos Fernández) Prove Lemma 6.1.5
147 :check: (Jeremy Tan) Prove Lemma 6.1.6
148 :check: (María Inés de Frutos Fernández, Joris Roos) Prove Lemma 6.1.3
149 :check: (Jeremy Tan) Prove Lemma 6.1.4
150 :check: (María Inés de Frutos Fernández) Prove Proposition 2.0.3

151 :check: (Jeremy Tan) Prove Lemma 3.0.1 (has 5 independent parts, mostly easy)
152 :check: (Floris van Doorn) Prove the second-countability of Θ
153 :check: (Floris van Doorn/Jeremy Tan) Prove Lemma 3.0.4
154 :check: (Jeremy Tan) Prove Lemma 3.0.3
155 :check: (Jeremy Tan) Prove Lemma 3.0.2
156 :check: (Jeremy Tan) Prove Theorem 1.0.3 (short)
157 :check: (Jeremy Tan) Prove Theorem 1.0.2 (the official main theorem)

158 :check: (Jasper Mulder-Sohn) (Part of Lemma 10.1.6) Prove measurability of simpleNontangentialOperator . After fpvandoorn/carleson#376 a simple proof is part of the blueprint (in the proof of Lemma 10.1.6).
159 :check: (Jeremy Tan) Modify KernelProofData so that it assumes (1.0.23) instead of (1.0.18) and fix the proof of Lemma 7.2.2 (also in the blueprint refer to (1.0.23) instead of (1.0.18))
160 :check: (Jeremy Tan) Replace 471a^3 + 4 by 472a^3 in the blueprint (various places in chapters 1, 3) and in carleson#C1_0_2.

ω :play: (Floris van Doorn) Ensure that the proof is actually sorry-free (depends on all tasks < ω) (this task is hopefully vacuous)
ω+1 :new: Go through some of the globally assumed type-class assumptions and check whether they are all actually used. (depends on ω)

[Floris van Doorn]

@Edward van de Meent have you made progress on task 102? Do you intend to finish it?
@Clara Torres Do you need help with task 138? Which lemmas have you been working on? Are there lemmas in this task that others can/should claim?

[Michael Rothgang]

#359 bumps Carleson to current mathlib: everything builds, but I sorried ~15 proofs where the fix was not as obvious.

[Michael Rothgang]

#360 does some follow-up golfing :tada:

[Notification Bot]

Aaron Hill has marked this topic as resolved.

[Edward van de Meent]

i'm very sorry for the radiosilence from my part, i had to focus on my masters courses. I did "finish" 102 (meaning the lemma has been proven in lean), but have yet to complete cleanup.

[Notification Bot]

Aaron Hill has marked this topic as unresolved.

[Aaron Hill]

Sorry, didn't mean to do that

[Michael Rothgang]

Feel free to open a PR already. Some clean-up can also happen after the lemma was merged.

[Michael Rothgang]

(And not all code in Carleson needs to be at mathlib standards.)

[Jeremy Tan]

Lemma 7.6.2 is complete at fpvandoorn/carleson#355.

(By the way, the branch name naafiri is a League of Legends character.)

[Jeremy Tan]

Lemma 7.4.6 done in the same PR

[Jasper Mulder-Sohn]

PR for Lemma 10.1.6: fpvandoorn/carleson#362, still needs some details

In the meantime, can I follow through with 10.1.7 and 10.1.8?

[Jeremy Tan]

Lemma 7.4.5: fpvandoorn/carleson#364

[Clara Torres]

Floris van Doorn ha dicho:

Clara Torres Do you need help with task 138? Which lemmas have you been working on? Are there lemmas in this task that others can/should claim?

I'm too busy with my work so I'm taking a break from Lean rn

[Jeremy Tan]

@Michael Rothgang When I proved Lemma 7.4.6 I added a lemma adjoint_tile_support2_sum that can help you with the missing part of Lemma 7.4.4

[Floris van Doorn]

I added a task 158 (and renumbered the old 158/159), which is needed in Lemma 10.1.6 (which is otherwise complete). It asks to formalize a tricky measurability-proof.

[Michael Rothgang]

Jeremy Tan said:

Michael Rothgang When I proved Lemma 7.4.6 I added a lemma adjoint_tile_support2_sum that can help you with the missing part of Lemma 7.4.4

Thanks, that was helpful. fpvandoorn/carleson#372 completes the proof of Lemma 7.4.4

[Michael Rothgang]

And fpvandoorn/carleson#371 bumps to mathlib 4.20.0.

[Floris van Doorn]

Floris van Doorn said:

I added a task 158 (and renumbered the old 158/159), which is needed in Lemma 10.1.6 (which is otherwise complete). It asks to formalize a tricky measurability-proof.

fpvandoorn/carleson#376 will add this argument to the blueprint, making task 158 an easy task.

[Harald Husum]

I can't see Proposition 2.0.6 in the task list. Why is that?

[Floris van Doorn]

Because it's basically already done (for a while). The reason that we haven't marked the bubble green yet is to indicate that there are still some sorry's in its proof, which are part of tasks 116+117. So once those are finished, we can mark Proposition 2.0.6 green.

[Jeremy Tan]

fpvandoorn/carleson#380: this fills in the last sorry in Lemma 6.1.5, and changes many exponents in constants to be ℕ-valued. It does not change the actual constant values

[Jeremy Tan]

It is done

[Jeremy Tan]

image.png

[Notification Bot]

2 messages were moved here from #Carleson > Problems in the forest operator proposition by Jeremy Tan.

[Jeremy Tan]

@Edward van de Meent can you make a PR with your code for Task 102 (Lemma 7.7.2)? Even if it isn't polished

[Floris van Doorn]

Jeremy Tan said:

It is done

That is fantastic! That means that modulo Edward pushing his work on Lemma 7.7.2, we're done with chapter 7, which is the most technical part of the blueprint!

[Jeremy Tan]

I've pushed another commit to fpvandoorn/carleson#379: prior to that commit the adjoint operators were defined on the ForestOperator side of things, but Antichain needs them as well, so I moved (adjoint)Carleson(Sum) to a common file that ForestOperator and Antichain now import without otherwise importing from each other

[Floris van Doorn]

Thanks, I merged it.

[Jeremy Tan]

Lemma 6.1.4: fpvandoorn/carleson#385

[Jeremy Tan]

Lemma 6.1.6 proved in the same PR

[James Sundstrom]

I'll take Lemma 10.2.5 (task 138).

[Jeremy Tan]

Lemma 10.2.4: fpvandoorn/carleson#393

[Jeremy Tan]

Lemma 3.0.4: fpvandoorn/carleson#394

[James Sundstrom]

Claiming Lemma 10.2.6 (task 139).

[Jasper Mulder-Sohn]

Lemma 10.1.7 (and finalizing 10.1.8): fpvandoorn/carleson#398

Let me claim the remainder of Section 10.1, i.e. tasks 127 and 158.

[James Sundstrom]

Claiming Lemma 10.2.2 (task 136)

[James Sundstrom]

Claiming Lemma 10.2.7 (task 140)

[Jeremy Tan]

Lemma 3.0.3: fpvandoorn/carleson#413

[Jasper Mulder-Sohn]

Lemma 10.0.2: fpvandoorn/carleson#417
And I'll claim Theorem 10.0.1 as well (constants need to be adjusted)

[Jeremy Tan]

Lemma 3.0.2: fpvandoorn/carleson#418

[Jeremy Tan]

Lemmas 10.2.8, 10.2.9 and 10.0.3: fpvandoorn/carleson#421

[Jeremy Tan]

Already mentioned in the other thread, but Lemma 7.2.2 is fixed to use (1.0.23) in fpvandoorn/carleson#423

[Jeremy Tan]

Also fpvandoorn/carleson#420 seems ready

[James Sundstrom]

Lemma 10.2.7 (task 140): fpvandoorn/carleson#425
Lemma 11.3.1 (task 128): fpvandoorn/carleson#431

[Jeremy Tan]

Lemma 3.0.1 and Theorem 1.0.3: fpvandoorn/carleson#429

[Michael Rothgang]

After fpvandoorn/carleson#430 (by @Jim Portegies), the real interpolation theory is sorry-free again, and fully generalised to enormed spaces :tada: :partying_face:

[Johan Commelin]

I sometimes wonder whether we should rename them to enormous spaces.

[Jeremy Tan]

Although of course we have had other contributors I feel like this whole project has been carried on the backs of four people: Jeremy, James, Jasper and Jim

[Jeremy Tan]

After my 3.0.1/1.0.3 PR gets merged the only task of major significance left will be 1.0.2 – the apex predator

[Jeremy Tan]

Michael Rothgang said:

After fpvandoorn/carleson#430 (by Jim Portegies), the real interpolation theory is sorry-free again, and fully generalised to enormed spaces :tada: :partying_face:

fpvandoorn/carleson#433 marks Hardy–Littlewood as finished

[Floris van Doorn]

Jeremy Tan said:

Although of course we have had other contributors I feel like this whole project has been carried on the backs of four people: Jeremy, James, Jasper and Jim

There are definitely several other people that have made major contributions, especially before last month.

[Jeremy Tan]

The fixed 10.2.8, 10.2.9 and 10.0.3 are now up at fpvandoorn/carleson#421

[Jeremy Tan]

And you probably suspected this, but I'm claiming 1.0.2

[Sébastien Gouëzel]

Can I claim 11.3.5 and 11.1.6?

[Floris van Doorn]

Btw, if someone is still looking for a new task, Maria mentioned that someone can take over Lemma 6.1.3 (task 148). There is already some partial work on this formalized, but Maria has no further local work on it.

[Floris van Doorn]

Current status: In fpvandoorn/carleson#436 I did some cleanup of the sorry's in the repository. After this PR, there are 26 sorry's in the repository (+ 23 sorry's that are for "stretch goals" proving some versions of classical_carleson that are stronger than the blueprint's version, but still already known in the 1960).
These 26 sorry's are all part of the 8 remaining tasks that are not marked as complete yet. There are only 7 non-green nodes in the blueprint, because we marked Lemma 10.0.2 as completed (perhaps a bit prematurely), even though it still depends on 2 sorry's in the formalization.

In short: all sorry's in the repository are accounted for.

[Joris Roos]

@Floris van Doorn @María Inés de Frutos Fernández I'd be happy to take over Lemma 6.1.3

[Floris van Doorn]

Jasper Mulder is busy with other things for the next few weeks. So if someone wants to take over the 2 1 remaining sorry's used in Lemma 10.0.2 (task 127) or the proof of Theorem 10.0.1 (task 144), feel free to do so.

[Jim Portegies]

Floris van Doorn said:

Jasper Mulder is busy with other things for the next few weeks. So if someone wants to take over the 2 1 remaining sorry's used in Lemma 10.0.2 (task 127) or the proof of Theorem 10.0.1 (task 144), feel free to do so.

I wouldn't mind taking over both (but if anyone else wants a task we can share)

[James Sundstrom]

@Jim Portegies I can take Lemma 10.0.2 if you haven't started it yet.

[Sébastien Gouëzel]

PR for Lemma 11.3.5 at carleson#445. I think there was a sign mistake in the blueprint, so I've made a (nontrivial) change to a definition and several statements, see the PR description for more on this.

[Jim Portegies]

James Sundstrom said:

Jim Portegies I can take Lemma 10.0.2 if you haven't started it yet.

I'm sorry @James Sundstrom I think I just finished it

[Jim Portegies]

I believe #446 finishes Task 127

[Jim Portegies]

@James Sundstrom I haven't started task 144 yet, do you want to take over that one instead?

[James Sundstrom]

@Jim Portegies No need to apologize. You can do task 144 if you want, or leave it for me. I'm fine either way.

[Jeremy Tan]

Theorem 1.0.2 is done.
fpvandoorn/carleson#435

[Floris van Doorn]

Thanks! That is the main result finished (though not yet all dependencies).
I added a small task 160: the main result now uses $471 a ^ 3 + 4$ in the constants, which suggests a much more diligence in the constant than we have actually put into it. Can someone replace it by $472a^3$ in the blueprint and the formalization?

[Jeremy Tan]

Floris van Doorn said:

Thanks! That is the main result finished (though not yet all dependencies).
I added a small task 160: the main result now uses $471 a ^ 3 + 4$ in the constants, which suggests a much more diligence in the constant than we have actually put into it. Can someone replace it by $472a^3$ in the blueprint and the formalization?

fpvandoorn/carleson#448

[Edward van de Meent]

unfortunately my proof has been broken because BoundedCompactSupport f no longer means f is bounded :sad:
(yes, i had it coming since i didn't make a pr)

[Edward van de Meent]

concretely, it means i have to do a bunch of math gymnastics to convince lean that the adjointCarlesonSum is bounded by 1, rather than just being BoundedCompactSupport

[Edward van de Meent]

(which even i'm not convinced of)

[Edward van de Meent]

it's actually seems to be the same issue as the one i mentioned at the start of #Carleson > 7.7.2

[Edward van de Meent]

truly and honestly, i don't understand why these things are written as $|f| \leq \textbf{1}_F$ rather than $\text{support}(f)\subseteq F$ in lean.

[Sébastien Gouëzel]

Because that's not the same: you are assuming both that the support is included in F, but also that f is bounded by 1 there.

[Edward van de Meent]

i know, but at 7.3.1, only the support part is used!!!

[Sébastien Gouëzel]

But that's in the assumptions of the statements, right? So it should only make your life easier (because checking integrability will be trivial, for instance)

[Edward van de Meent]

wdym?

[Edward van de Meent]

the proof of 7.7.2 relies on being able to apply 7.3.1 with f := adjointCarlesonSum f' with BoundedCompactSupport f' and |f'| \le F.indicator (or whatever the variables are called). i used to be able to get around that by using that the value of the adjoint carleson sum scales with f, and the fact that if f is bounded(compactsupport) then so is adjointCarlesonSum ..., so we get to scale with an actual bound of adjointCarlesonSum ... to fit it into the box of F.indicator.

[Edward van de Meent]

however, it seems like now i have to extract the more general versions of the inequalities of 7.3.1 to fix my proof

[Sébastien Gouëzel]

Ah, I get it: you're not proving 7.3.1, you're using it. And then indeed you need to check that your functions are bounded. But isn't that the case in the proof of 7.7.2? I see that assumption h2g saying that g is bounded there.

[Edward van de Meent]

well... g is, but maybe G.indicator (adjointCarlesonSum g) not.

[Edward van de Meent]

but we can prove that the support is right for that second one

[Sébastien Gouëzel]

Isn't adjointCarlesonSum a finite sum of things which are all bounded?

[Sébastien Gouëzel]

(by BoundedCompactSupport.bddAbove_norm_adjointCarleson)

[Edward van de Meent]

ah... i couldn't find that lemma. Still, there is no reason why the assumptions to 7.3.1 are as stringent as they are.

[Edward van de Meent]

and it makes the proof more difficult

[Edward van de Meent]

(imo)

[Edward van de Meent]

particularly since you need to do a scaling trick to get it bounded to a concrete value

[Sébastien Gouëzel]

Well, the strong assumptions of 7.3.1 will make its proof easier, but its application harder, as always. I think it would make sense to deduce a version of 7.3.1 assuming just that the function is bounded by C * 1_F from the current version of 7.3.1, and then you would apply this new version in your proof of 7.7.2.

[Edward van de Meent]

not at all... the change in number of lines in the proof of 7.3.1 is 0 (on my current branch)

[Edward van de Meent]

because in each case, the actual proof they want is x \notin G -> g x = 0

[Edward van de Meent]

so it doesn't make the proof of 7.3.1 easier.

[Sébastien Gouëzel]

Then I think you can definitely change the assumption to support g \subseteq G there!

[Edward van de Meent]

ok, i managed to get a working version again, but unfortunately my change to the definition of C7_7_2_1 and C7_7_2_2 (to make them depend on previous constants) seems to break some proofs later in the file...

[Edward van de Meent]

in particular, it breaks the proofs of le_sq_G2_0_4 and forest_operator_f_main

[Sébastien Gouëzel]

If the issue is just that we should adjust the constants downstream, I'm sure @Floris van Doorn would already be happy with your current proof, and a sorry where there is an incompatibility due to the mismatch in the constants. This can be fixed in another task.

[Edward van de Meent]

i made a draft PR at carleson#449

[Sébastien Gouëzel]

(There is a weird change to the file TileStructure.lean in your PR)

[Edward van de Meent]

ah, oops

[Edward van de Meent]

that's an artefact from rebasing, it should be fixed now

[James Sundstrom]

@Jim Portegies I've started on task 144, but happy to compare notes if you've been working on it too.

[Jeremy Tan]

Sébastien Gouëzel said:

If the issue is just that we should adjust the constants downstream

I believe that the change in 7.7.2's constants should not affect C2_0_4, because the dominant term comes from row_correlation with its 470a^3 whereas the adjusted 7.7.2 constants only have 303a^3 at most

[Joris Roos]

Lemma 6.1.3: https://github.com/fpvandoorn/carleson/pull/438

[Edward van de Meent]

Jeremy Tan said:

Sébastien Gouëzel said:

If the issue is just that we should adjust the constants downstream

I believe that the change in 7.7.2's constants should not affect C2_0_4, because the dominant term comes from row_correlation with its 470a^3 whereas the adjusted 7.7.2 constants only have 303a^3 at most

sure, but surely it should have been defined in terms of the previous constants instead? that would have prevented this issue...

[Jeremy Tan]

Edward van de Meent said:

sure, but surely it should have been defined in terms of the previous constants instead? that would have prevented this issue...

No matter. I am currently preparing a tidied-up version of your PR, one that does not change the indicator arguments, and will credit you in that PR

[Edward van de Meent]

why are you reverting that change?

[Sébastien Gouëzel]

We should definitely keep the change: it's strictly better than the current version because the proof is the same, and the lemma has then weaker assumption so it's easier to apply.

[Jeremy Tan]

Because that way I can reuse helper lemmas that I myself wrote for the other Section 7 lemmas that I did

[Jeremy Tan]

(exists_scale_factor_of_bddAbove_range, which gets around the ‖f x‖ ≤ F.indicator 1 x restriction, and sum_sq_eLpNorm_indicator_le_of_pairwiseDisjoint, and eLpNorm_two_eq_enorm_integral_mul_conj…)

[Sébastien Gouëzel]

The point of Edward is that all this is completely unneeded for the task at hand!

[Edward van de Meent]

also, i'd like to note that i only changed some internal parts of the lemmas that form 7.3.1, and depend on those. the "original" statements are still there, so if you depend on those it shouldn't matter, i think?

[Edward van de Meent]

in particular, the file QuantativeEstimate compiles...

[Jeremy Tan]

I've pushed a WIP to fpvandoorn/carleson#450. I have to be AFK now, my mother is pulling me out of the house for a walk

[Jeremy Tan]

@Edward van de Meent I'm back. I've completed the rest of 7.7.2 in fpvandoorn/carleson#450 and have verified that forest_union is sorry-free with it.

My main concern with your PR is that you're reinventing the wheel, stating new helper lemmas instead of reusing existing ones. It turns out there's some truth to this – adjoint_refined_density_tree_bound1 is essentially the same as Lemma 7.4.2 (in my PR I've modified the body of the latter lemma to reflect this)

[Edward van de Meent]

If that is how you felt about my proof, you could've just left a review on the pr... :neutral:

[Edward van de Meent]

No need to run off and make a pr of your own

[Jeremy Tan]

The sum of the improvements I spotted ended up being too big for me to leave a review on your PR.

Nevertheless, I gave you a chance to prove the lemma yourself and you have done so – so I congratulate you for that. I did not start on my PR until I saw yours, and thus I have given due credit

[Edward van de Meent]

this is not about credit; you have made a PR for a task you did not claim.

[Edward van de Meent]

what's worse, the task for which you made a PR was already claimed

[Jeremy Tan]

On second thought I'll add the generalisation to densities_tree_bound_aux from your PR to mine

[Jeremy Tan]

Edward van de Meent said:

what's worse, the task for which you made a PR was already claimed

There is no absolute bar preventing me from making a PR for an already claimed task. But sure, I will try and leave reviews on yours

[Edward van de Meent]

thanks, i really appreciate it. :+1:

[Jeremy Tan]

Treat my PR as an exploration of what could be. Anything that doesn't make it into your PR will be merged in a later commit

[Jeremy Tan]

On a side note, we now have sorry-free PRs for all remaining unsolved nodes in the dependency graph (blue) except 11.1.6 in the classical reduction

[Jeremy Tan]

We could have metric space Carleson sorry-free by Bastille Day

[Jeremy Tan]

@Edward van de Meent I have left review comments on your PR

[Edward van de Meent]

thanks, these are great! i'm going over them right now

[Sébastien Gouëzel]

Jeremy Tan said:

On a side note, we now have sorry-free PRs for all remaining unsolved nodes in the dependency graph (blue) except 11.1.6 in the classical reduction

Sorry-free PR for 11.1.6 at https://github.com/fpvandoorn/carleson/pull/452

[Jeremy Tan]

This is brilliant. I will have to pull in all five PRs locally and see if classical_carleson is sorry-free after I have my dinner

[Jeremy Tan]

We have done it.

image.png

fpvandoorn/carleson#453

[Jim Portegies]

James Sundstrom said:

Jim Portegies I've started on task 144, but happy to compare notes if you've been working on it too.

Lol I missed this (my fault), your solution is much more compact than mine though.

[James Sundstrom]

@Jim Portegies Well, that makes me feel better about how ugly mine is.

[Floris van Doorn]

Thanks for this present after I've taken a break this weekend. This is great! I'll review/merge the open PRs today.

@Jeremy Tan I already warned you about this last week, but don't open PRs with material that replaces what other people are doing at the same time. That is demotivating for others.

[Floris van Doorn]

@Edward van de Meent The BoundedCompactSupport refactor was a bit unfortunate, and indeed caused fallout in a few places where (aspects of) the old definition were more convenient, because on a set of measure 0 the functions can now be unbounded.

[Edward van de Meent]

fpvandoorn/carleson#449 has been merged :tada:

[Jeremy Tan]

Edward van de Meent said:

fpvandoorn/carleson#449 has been merged :tada:

But you forgot to add \leanok to the blueprint; I do that in fpvandoorn/carleson#466

[Jeremy Tan]

I finally apply the changes I intended to make in fpvandoorn/carleson#450 in fpvandoorn/carleson#478