Zulip Chat Archive

Stream: new members

Topic: Lp spaces


view this post on Zulip Rémy Degenne (Nov 12 2020 at 11:41):

Hello,
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).

view this post on Zulip Kevin Buzzard (Nov 12 2020 at 12:18):

@maintainers :upvote:

view this post on Zulip 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 BnB_n is a positive sequence of real numbers, and any series un\sum u_n with un<Bn\|u_n\| < B_n for all nn is converging. Then the space is complete.

view this post on Zulip 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.

view this post on Zulip Reid Barton (Nov 12 2020 at 12:59):

@Rémy Degenne invite sent!

view this post on Zulip Rémy Degenne (Nov 12 2020 at 12:59):

Thanks!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip Alex J. Best (Nov 12 2020 at 18:24):

You can write #lint at the bottom of each file you want to lint.

view this post on Zulip Rémy Degenne (Nov 12 2020 at 18:25):

Thank you !

view this post on Zulip 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!

view this post on Zulip 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!

view this post on Zulip 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