[Merged by Bors] - feat(measure_theory/lp_space): add more lemmas about snorm

[RemyDegenne]

---

[sgouezel]

The additions in the PR look good to me.

I have one design question, though. The definitions we have currently are given for real p. Hoever, the case p = \infty is also an important one, and many statements hold uniformly over all positive p, including \infty. Many results (including duality, convolution, interpolation, and so on) can be formulated in this extended setting. So, I wonder if it would make sense to define snorm f p \mu more generally for p : ennreal, using the formula you have given for 0 < p < \infty, and for p = 0 the norm would be 0 if the function is almost everywhere measurable and \infty otherwise, and for p = \infty this would be the usual L^\infty-norm. This would require a non-trivial refactoring, but in the long run I have the impression this would be a move in the right direction. I am asking now because, the more material you add, and the harder the refactor will be.

[RemyDegenne]

My first attempt at defining those spaces had p : ennreal (or maybe nnreal?) but working with a non-real exponent is hell. We have rpow, but we don't have ennreal_pow : ennreal -> ennreal -> ennreal. The exponent has to be converted everywhere.

But I agree that including the infinite exponent case would be good. On top of that, many non-negativity hypotheses on p could be removed.

I'll experiment with it... and maybe define ennreal_pow, if that is what we need.

[RemyDegenne]

I think that I answered too fast and that the conversion between ennreal and real is in fact not an issue. if I understand correctly, what you suggest is a snorm f (p:ennreal) µ with three sub-cases, in which the main case is what I have been doing until now. So I can convert p to a real in that definition and there is no issue of ennreal exponent.

[RemyDegenne]

I don't think that it is necessary to have a special case for p=0.
The difference between your proposal and what I did in that case is that you propose a snorm that is finite (0) iff the function is ae_measurable, while it currently is 1 for all functions.
I think it does not matter because the definition of mem_Lp is "ae_measurable and snorm finite". The functions which are not ae_measurable are excluded from L0 anyway, so the value of snorm for these functions does not matter.

I'll experiment with a two-cases definition, R+infinity.

[sgouezel]

You're right for p = 0 that requiring ae_measurable is not important. However, having the norm of all functions to be zero is nicer, because it gives snorm p (c f) = c snorm p f for all p.

As for ennreal_pow, as you point out in your later message this is not necessary as one would only take the powers when the exponent is real (and (x^\infty)^0 can not be turned in something usable in any situation).

[RemyDegenne]

Indeed having snorm f 0 µ = 0 would be nicer for that reason. Then I'll adopt the 3 cases approach.

Should we merge this PR and have all the design changes in a next one?

[sgouezel]

Yes, let's merge this one already.
bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

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