## Stream: new members

### Topic: Lp spaces

#### 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).

#### Kevin Buzzard (Nov 12 2020 at 12:18):

@maintainers :upvote:

#### 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 $B_n$ is a positive sequence of real numbers, and any series $\sum u_n$ with $\|u_n\| < B_n$ for all $n$ 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!

Thanks!

#### 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.

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