[Merged by Bors] - feat(topology/metric_space/pi_Lp): L^p distance on finite products

[sgouezel]

L^p edistance (or distance, or norm) on finite products of emetric spaces (or metric spaces, or normed groups), put on a type synonym pi_Lp p hp α to avoid instance clashes, and being careful to register as uniformity the product uniformity.

---

Blocked by #2988

[gebner]

A very general question, and I hope I didn't miss an explanation on Zulip: is there a reason the Lᵖ-norm is only defined here for the special case of functions on finite measure spaces with the counting measure? Are there issues because these are dependent products?

[sgouezel]

The goal here is to show that the topology defined by the L^p norm is the same as the product topology. This is only true for finite products.

We will definitely need to define the L^p space for functions over a base with a measure (probably in a non-dependent setting), but the measure-theory part of mathlib is not completely ready yet.

[PatrickMassot]

It would be nice to have a global documentation for this uniformity juggling thing. Maybe you could also add a note discussing the two confusing interpretations: measure theoretic L^p that confused Gabriel but also the potential confusion about norm spaces since I guess people could complain the statement should be a special case equivalence of norms on R^n if they read the context too quickly. At the proof level one could also argue that one could use equivalence of norms after sending everything in some R^n, but we wouldn't get the explicit Lipschitz constants that you derive here, so maybe this is also worth one line of implementation notes.

bors d+

[bors]

✌️ sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[PatrickMassot]

Sébastien doesn't seem to like delegation, so let's:
bors r+

[bors]

👎 Rejected by label

[gebner]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests and docs

[sgouezel]

Hey, I was not done with the comments ! :-) Followup in #3070