new member

Stream: Carleson

[Clara Torres]

Hi, I hope it's okay to post here. I'm new to Lean4, did the natural number game and a good chunck of MIL. I have a background in analysis. I'm thinking if I can contribute to the Carleson project (and where should I go to get started), or if I should study more Lean before starting.

[Floris van Doorn]

Welcome! If you've worked through the analysis chapters of MIL then I think you can contribute (though it might be hard). I posted some new tasks recently. Task 134 in the outstanding task list is very elementary, so feel free to claim it.

[Kevin Buzzard]

I've had relatively new people with an interest in number theory contributing to FLT, I think it's a great idea to find yourself a project and see if you can help. The community here is super-helpful and welcoming and will probably be very happy to answer questions even at a basic level. In my mind the best way to learn after NNG and MIL is to find a project and to get working on it, it might be hard at first but you'll begin to learn a corner of the library which is a really important next step after you've looked at the basic literature.

[llllvvuu]

My next step after NNG was to do some elementary lemmas on some projects. This was very helpful to learn about “real” mathlib usage (and about math, hah)

[Clara Torres]

Hi, I finished with the book and feel ready to start trying to contribute. Task 134 is very elementary, but before I can do a task I need to know how to start, i.e. should I clone a repo, how is this organized? I have never done code with more people.

And also specific to the task, the description says to prove something and add some lemmas for bla bli bla. I'm a bit lost rn.

[Ruben Van de Velde]

Clone https://github.com/fpvandoorn/carleson , yes

[Floris van Doorn]

There are instructions on the page https://github.com/fpvandoorn/carleson on how to get the project locally, so that you can contribute.
If you've never used Git before, you might want to read this on how to work with git: https://leanprover-community.github.io/contribute/index.html
That is for Mathlib. For the Carleson project it's a bit different, since you have to create your own fork of the repository (on Github), and then (once you've done some work) push to your own fork.
The instructions here might also be helpful: https://github.com/fpvandoorn/LeanCourse24/tree/master/LeanCourse/Project#git-instructions

[Clara Torres]

Ok so I managed to fork and build the thing, and I am trying to do task 134. I understand that there is a missing lemma like wnorm_const_smul_le

[Clara Torres]

Edit: fixed

I tried to write this, but it fails to synthesize

lemma wnorm_const_smul_le {𝕜 E α : Type*} [NormedAddCommGroup E] {_x : MeasurableSpace α}
    {p p' : ℝ≥0∞} {μ : Measure α} {c : ℝ≥0}
    [NormedRing 𝕜] [MulActionWithZero 𝕜 E] [IsBoundedSMul 𝕜 E] (c : 𝕜) :
    wnorm (c • f) p μ ≤ ‖c‖₊ * wnorm f p μ := by
  sorry

[Edward van de Meent]

do use #backticks please, it helps make code more readable

[Edward van de Meent]

(you can edit your original message and put them in)

[Floris van Doorn]

Sorry for the late reply. I took a short holiday for a long weekend.

The problem here is that you haven't specified the type of f. If you add the argument {f : α → E}, then it will work as expected. Without specifying the type of f, Lean will take the f from the variable lines, so it will have different domain/codomain.
This should work:

lemma wnorm_const_smul_le {𝕜 E α : Type*} [NormedAddCommGroup E] {_x : MeasurableSpace α}
    {p p' : ℝ≥0∞} {μ : Measure α} {c : ℝ≥0} {f : α → E}
    [NormedRing 𝕜] [MulActionWithZero 𝕜 E] [IsBoundedSMul 𝕜 E] (c : 𝕜) :
    wnorm (c • f) p μ ≤ ‖c‖₊ * wnorm f p μ := by
  sorry

[Clara Torres]

Yes, thank you

[Clara Torres]

I am trying to prove

lemma wnorm_const_smul_le {𝕜 E α : Type*} [NormedAddCommGroup E] {_x : MeasurableSpace α}
    {p : ℝ≥0∞} {μ : Measure α} {f : α → E}
    [NormedRing 𝕜] [MulActionWithZero 𝕜 E] [IsBoundedSMul 𝕜 E] (k : 𝕜) :
    wnorm (k • f) p μ ≤ ‖k‖₊ * wnorm f p μ := by

But it is false because in the case k = 0, p = 0, it fails. I imagine there are several possible fixes, but I wanted to ask for opinions on how best to handle this.

I guess we never care about the weak norm in L^0 (doesn't make much mathematical sense, but it is defined for implementation reasons).

[Floris van Doorn]

Good point! Please add the condition that p is nonzero (and similar conditions to carleson#MeasureTheory.HasWeakType.const_smul, as needed).

[Floris van Doorn]

Indeed, in Lean we usually decide to define functions/predicates on their whole domain, and then for theorems about them, we add hypotheses that values are in the mathematically-sensible domain as needed.

[Clara Torres]

Ok, now I want to use

lemma distribution_smul_left {f : α → E} {c : 𝕜} (hc : c ≠ 0) :
    distribution (c • f) t μ = distribution f (t / ‖c‖₊) μ

But the type does not quite match. This lemma is written for

[NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]

and the first and third types are missing. Am I missing something or should I change something?

[Floris van Doorn]

When stating the lemma, I did not think super carefully about the right generality. You can try to generalize the type-classes of distribution_smul_left, and see if that works. Otherwise (more likely) you can replace the type-classes of the new lemmas by the type-classes in the statement of distribution_smul_left

[Clara Torres]

I think

[NormedRing 𝕜] [MulActionWithZero 𝕜 E] [IsBoundedSMul 𝕜 E]

should be enough but then the current proof of distribution_smul_left does not work anymore. I can try to redo it.

More of a meta question: how hard should we try to do things in the absolute most generality possible?

[Kevin Buzzard]

I find it an interesting exercise when doing algebra in lean to try and state my theorems in the most general generality, but algebra is a topic where we have many obscure definitions not found in the literature, such as groups with zero and subtraction monoids, which makes this kind of problem not too difficult. Away from algebra I would imagine that things get more tedious so I would not bother too much about this, especially if your goal is to help with the Carleson project in a practical way.

[Floris van Doorn]

This is an interesting question without a unique best answer. For this project, clearly having NontriviallyNormedField + NormedSpace is fine, and I'm happy to accept such a contribution.

I recommend the following: try to find a proof of distribution_smul_left in the general case that isn't significantly harder than the current proof. If that fails because some Mathlib lemma has unnecessarily strong assumptions, just add a note "TODO: this can probably be done using the assumptions ..., but it requires generalizing lemmas A and B to this setting" and leave it as-is.

[Clara Torres]

I tried, and it made me realize you really need k to be a field to have the expected equality.

[Clara Torres]

Ok, I finished the task in my local file, modulo reorganizing some variable declarations that I'm not entirely comfortable with.

Next step is to make a PR I imagine. How should I proceed?

[Michael Rothgang]

So you question is "how do I create a PR"?

[Clara Torres]

My question is: "if I google how to create a PR is that going to work for this project"

[Clara Torres]

I expect some conventions to be in place here, and have never worked in anything similar

[Michael Rothgang]

Aha! I think the answer is yes, the Carleson project uses the standard github model.

[Michael Rothgang]

(In short: fork the repo, create a branch on your fork, commit your changes there, push those, then open a PR.)

[Michael Rothgang]

mathlib uses a bespoke model (so it's good you asked), but projects depending on mathlib usually do not.

[Clara Torres]

Imports are out of date and must be rebuilt; use the "Restart File" command in your editor.

I created a new branch to start another task, and I get this error everywhere. If I restart the file, it tries to rebuild the entire Mathlib. I feel this shouldn't happen.

[Kevin Buzzard]

Try lake exe cache get to hopefully download a fully built mathlib from the cloud, and hopefully your problems will go away.

[Michael Rothgang]

Rebuilding all of mathlib, when you're in a project depending on mathlib, should not happen. (Then you should run lake exe cache get, as Kevin says.)

[Michael Rothgang]

This warning can happen (and is expected) when you modify a more basic file X in (say) the Carleson project, and then want to edit a file Y in Carleson which imports X (directly or transitively). Then, that warning is just telling you "I need to rebuild this file and any intermediate files", and doing that rebuilding is just fine.

[Clara Torres]

I ran lake exe cache get and that downloaded about 1200 of the 2500 things that are needed when I do lake build, is this normal?

[Michael Rothgang]

lake exe cache get should download everything from mathlib (but not from the carleson project). If you look at the terminal output from lake build, it should tell you if you're building mathlib files or carleson files.

[Michael Rothgang]

What does it say?

[Clara Torres]

It's building Mathlib files

[Kevin Buzzard]

Have you edited any mathlib files? Then the cache won't work.

[Kevin Buzzard]

Are you sure it's building mathlib files and not Carleson files?

[Patrick Massot]

This kind of thing is hard to debug remotely, but I’m sure you can find people to do a quick video meeting helping you through this if needed. I can do it if I’m around when you write “let’s do it now”.

[Kevin Buzzard]

The nuclear option is: go to the command line, to the root directory of the Carleson project. Delete the .lake directory (e.g. rm -rf .lake), then lake exe cache get to get it back, and see if this solves the problem.

[Clara Torres]

resetting everything worked, thank you

[Clara Torres]

I was trying to start doing task 138 (21 "easy" sorry's in proof of Lemma 10.2.5)

[Clara Torres]

I don't understand how Lemma 10.2.1 is formalized, in particular, how to provide the hypothesis 4 <= a.

[Clara Torres]

This is just a line in the proof, and conceptually easy, but I'm missing something.

[Sébastien Gouëzel]

There is a lemma four_le_a X.

[Clara Torres]

Thank you. However it fails to synthesize PreProofData a ?m.24978 ?m.24979 ?m.24980 ?m.24981 ?m.24982 ?m.24983

[Clara Torres]

I just tried in the naive way:
have : 4 ≤ a := four_le_a X

[Floris van Doorn]

Oh, oops. I might have forgotten the assumption 4 <= a in the statements of Section 10.2. Please just add the assumption (ha : 4 ≤ a) to your lemma (or all lemmas in Section 10.2)

[Floris van Doorn]

I added the assumptions in fpvandoorn/carleson#292

[Clara Torres]

Oh I see, thank you! I will get to it in a couple days

[Sébastien Gouëzel]

In the current dependency graph, it looks like the right part on classical Carleson does not depend on the left part (fancy Carleson). For instance, nothing seems to depend on finitary-Carleson. Is it worth adding a dependency somewhere, to reflect more accurately the mathematics?

[Floris van Doorn]

Thanks for the remark. I need to add the dependencies in the new chapter 3.

[Floris van Doorn]

Should be fixed in fpvandoorn/carleson#303