[Merged by Bors] - feat(measure_theory/lp_space): Define Lp spaces

[RemyDegenne]

Define the space Lp of functions for which the norm raised to the power p has finite integral.
Define the seminorm on that space (without proof that it is a seminorm, for now).

Add three lemmas to analysis/special_functions/pow.lean about ennreal.rpow

[sgouezel]

I have a design question, as I explain in one of the comments: I don't see what use the subtype ℒp would have in the applications (contrary to the subtype Lp of almost everywhere defined functions, which is a normed space and with which one can do analysis) that could not be done as efficiently with the mem_ℒp predicate. Could you explain a little bit why you designed your PR like this?

[RemyDegenne]

I have removed the Lp type.
The PR now contains mainly the definition of the mem_LP property and of the quantity snorm, with a first few lemmas relating these two definitions.

[RemyDegenne]

To elaborate on the plan forward: my idea is to first have a sequence of PRs about the properties of mem_Lp, and only then to define the quotient space Lp of functions almost everywhere equal and prove properties of that type (which should be trivial consequences at that point).

[sgouezel]

I have a lot of minor comments, both about mathlib style and Lean tricks. It's normal, first PRs are always like that (and they are a great occasion to learn). But I am quite happy with the overall content, thanks!

[bryangingechen]

Note that there are still 2 unaddressed comments that have been unhelpfully hidden from view by GitHub. You can see them if you click on "2 hidden comments", or by visiting the "Files Changed" tab above.

[sgouezel]

bors r+
Thanks!

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests
• Lint style