[Merged by Bors] - feat(topology/metric_space/pi_lp): Holder and Minkowski inequalities in ennreal

[sgouezel]

Hölder and Minkowski inequalities for finite sums. Versions for ennreals.

---

The goal is to put the L^p norm on finite products of metric spaces (ultimately fixing the current definition of the Euclidean space in mathlib), but to keep things at a reasonable length this PR only contains the above inequalities.

The versions in reals and nnreals have been golfed and added in #3025, so there just remains the ennreal version (that I will need for the L^p distance on finite products of emetric spaces).

[urkud]

What's wrong with the current definition of the Euclidean space in mathlib? If you want it to be the L^2 space, then you'll need to refactor real inner product spaces to accept a has_norm (or normed_space?) instance and require ∥a∥²=inner a a.

[sgouezel]

The main flaw of the current euclidean space is that its topology is not (defeq to) the product topology.
We need to refactor it to take a norm, which is equal (but maybe not defeq) to sqrt (inner x x). So I should construct this (L^2) norm in some way, so let's do all the L^p, and prove for all of them that they induce the product topology. I have all this locally, and I will PR it in tiny bits.

[semorrison]

Is this ready to merge now? It looks fine to me.

[PatrickMassot]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Run tests and docs
• Build mathlib
• Lint mathlib