Lspace master

[affeldt-aist]

Motivation for this change

This is the same contents as the PR on Lp spaces except that it does not require MathComp master.

closes #1361

fixes #1360

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

I tried to write an exhaustive changelog. I also left a few easy comments that I might address later.

[affeldt-aist]

I tried to write an exhaustive changelog. I also left a few easy comments that I might address later.

I tried to address my own comments but I feel that there is still room for improvement because I am not sure about how the properties of Lp-norms are split between hoelder.v and lspace.v.

[affeldt-aist]

Oops... reals.v and discrete.v have been modified (Coq -> Corelib) :-(

[affeldt-aist]

I have rebased on master (since lebesgue_integral.v has been split in between, I thought that it is better to not let the PR diverge).
The changelog (which is not particularly small) seems to have rebased correctly.
There are less commits because commits related to interval_inference.v were also merged into master in between by @proux01 (e.g., 64b44f4)

[proux01]

Are the individual commits expected to make sense? (I would be a bit wary of squashing a +2000-500 lines single commit)

[affeldt-aist]

Are the individual commits expected to make sense? (I would be a bit wary of squashing a +2000-500 lines single commit)

What we could do to make progress is to extract from this PR the less controversial stuff (e.g., ess_sup_inf.v) and make it a different PR to rebase on. That would make for a meaningful commit. What do you think? @hoheinzollern @CohenCyril

[affeldt-aist]

Are the individual commits expected to make sense? (I would be a bit wary of squashing a +2000-500 lines single commit)

What we could do to make progress is to extract from this PR the less controversial stuff (e.g., ess_sup_inf.v) and make it a different PR to rebase on. That would make for a meaningful commit. What do you think? @hoheinzollern @CohenCyril

Moreover it will be useful for ongoing work that generalizes L-norm to p < 0.

[affeldt-aist]

Are the individual commits expected to make sense? (I would be a bit wary of squashing a +2000-500 lines single commit)

I do not think they make much sense.
The plan would rather be to:

1. extract from this PR all the lemmas of general interest that are non-breaking additions (in particular in classical and some in measure.v) as a separate PR
2. extract the ess_sup_inf.v as a separate PR (this is also non-breaking)
3. extract the addition of the {ae _, _} notation as a separate PR (this will cause the modification of some lemmas in lebesgue_integral_theory, charge.v, etc. but this is also uncontroversial)
4. the rest (changes to hoelder.v, etc.) would be a last PR where we can address the changes discussed during the last MathComp-Analysis dev meeting

@hoheinzollern