Convexity of powR

[hoheinzollern]

Motivation for this change

This change introduces:

• discrete lp spaces and correspondence lemmas with Lp spaces
• a specialization of hoelder for sums
• a further specialization for sums of 2 elements
• as a consequence of hoelder, we obtain the convexity of powR

Co-authored by: @affeldt-aist

Things done/to do

• added corresponding entries in CHANGELOG_UNRELEASED.md
• added corresponding documentation in the headers

Compatibility with MathComp 2.0

• I added the label TODO: HB port to make sure someone ports this PR to
  the hierarchy-builder branch or I already opened an issue or PR (please cross reference).

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[affeldt-aist]

CI is green.

[affeldt-aist]

We can maybe merge it for now as we will certainly come back to it anyway when preparing the PR #1000 about Minkowski's inequality. Moreover, the theory about powR is being used for another project that could benefit from having a release with more lemmas.

[affeldt-aist]

CI errors seem unrelated...

[affeldt-aist]

Here are the last lines for convenience:

build flags: -j2 SHELL=/nix/store/vqvj60h076bhqj6977caz0pfxs6543nb-bash-5.2-p15/bin/bash
/nix/store/0qcapxv1v78nridqcr37hkmp0r1hk9x2-coq-dev/bin/coq_makefile  -f Make -o Makefile.coq
make -f Makefile.coq --no-print-directory
COQDEP VFILES
COQC fingroup.v
COQC morphism.v
COQC perm.v
COQC presentation.v
File "./presentation.v", line 165, characters 0-62:
Error: A left-recursive notation must have an explicit level.```

[affeldt-aist]

@proux01 Am I right to think that the error messages are unrelated to the last commit? (CI was green before it but the error looks unrelated.)

[proux01]

@affeldt-aist yes, this is unrelated. Apparently we merged coq/coq#18031 without proper CI, sorry about that.

[affeldt-aist]

@affeldt-aist yes, this is unrelated. Apparently we merged coq/coq#18031 without proper CI, sorry about that.

Thanks for the quick answer!