Lp spaces

Stream: new members

[Rémy Degenne]

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]

@maintainers :upvote:

[Sebastien Gouezel]

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]

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]

@Rémy Degenne invite sent!

[Rémy Degenne]

Thanks!

[Reid Barton]

It sounds like you have material for several PRs; it's better to PR things separately, especially when they are independent.

[Johan Commelin]

Just to get a feel for the process, you might want to make a first PR with ~50 lines of code.

[Rémy Degenne]

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]

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]

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

[Rémy Degenne]

Thank you !

[Bryan Gin-ge Chen]

@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]

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]

Don't worry, this whole GitHub thing needs some time to get used to it.