Stream: new members
Topic: Lp spaces
Rémy Degenne (Nov 12 2020 at 11:41):
I have been proving things about Lp spaces (the spaces of functions with norm having finite integral when raised to the power p, not quotiented) and I would like to turn that work into a pull request.
Could I get access to non-master branches? My github name is RemyDegenne.
The main results are, depending on hypotheses : Lp spaces are add_comm_group; Hölder inequality for functions with values in nnreal; Minkowski inequality; Lp spaces are premetric_space; Lp spaces are vector_space.
Next step is to prove completeness, but I first need to learn how to use Cauchy sequences in lean. Can anyone point me to a file where Cauchy sequences are used?
After that, the plan is to have specialized results for L1 (but a lot is already done through the "integrable" statements) and mostly for L2 and to relate to the quotiented Lp, proving for example that it is then a metric_space (and inner_product_space for L2).
Kevin Buzzard (Nov 12 2020 at 12:18):
Sebastien Gouezel (Nov 12 2020 at 12:29):
To prove completeness, you could for instance use the criterion docs#metric.complete_of_convergent_controlled_sequences. Although it would probably be better to prove a criterion in terms of converging series, of the form: assume is a positive sequence of real numbers, and any series with for all is converging. Then the space is complete.
Rémy Degenne (Nov 12 2020 at 12:54):
Thanks for the tip!
I don't have a metric space but only a premetric one, but by looking under the hood very quickly it seems that all I need is an uniform space, and premetric space implies uniform space, so that works.
Reid Barton (Nov 12 2020 at 12:59):
@Rémy Degenne invite sent!
Rémy Degenne (Nov 12 2020 at 12:59):
Reid Barton (Nov 12 2020 at 13:02):
It sounds like you have material for several PRs; it's better to PR things separately, especially when they are independent.
Johan Commelin (Nov 12 2020 at 13:04):
Just to get a feel for the process, you might want to make a first PR with ~50 lines of code.
Rémy Degenne (Nov 12 2020 at 13:07):
Ok, I'll cut it into several pieces. Something like 0) basic definitions, 1) add_comm_group, 2) Hölder, 3) Minkowski + premetric_space (since Minkowski is the only difficulty), 4) vector space.
Rémy Degenne (Nov 12 2020 at 18:01):
So I've tried making a PR but I have linting errors, which is what I expected since I never checked that aspect. Is there a way to run the lint locally, and only on my new files?
I'd like to avoid waiting 1h before realizing that I forgot a docstring on a definition :)
Alex J. Best (Nov 12 2020 at 18:24):
You can write
#lint at the bottom of each file you want to lint.
Rémy Degenne (Nov 12 2020 at 18:25):
Thank you !
Bryan Gin-ge Chen (Nov 12 2020 at 19:54):
@Rémy Degenne it looks like you've been opening new PRs and then closing them again e.g. #4990 and #4991. The usual practice would be to push new commits to existing PR branches instead of creating a new branch and PR for every change. We're happy to help if you're having trouble with git / github, just let us know!
Rémy Degenne (Nov 12 2020 at 20:47):
Yeah sorry, I committed something to a branch for which I had a PR open, then closed it when I saw that the new changes were included in the PR (I discovered that a PR is about the branch and not a specific commit as I mistakenly thought). I should have simply reverted. The other one I'll just reopen tomorrow and work from there, hopefully without further mistakes!
Patrick Massot (Nov 12 2020 at 20:48):
Don't worry, this whole GitHub thing needs some time to get used to it.
Last updated: May 13 2021 at 05:21 UTC