refactor(analysis/normed_space/pi_Lp): make argument of pi_Lp a term of ℝ≥0∞ instead of ℝ

[j-loreaux]

This refactors pi_Lp so that the p argument has type ℝ≥0∞ instead of ℝ. There are several reasons for doing this:

1. It matches the design of lp.
2. We have pi_Lp ∞ β, so we can appropriately state various interpolation inequalities.
3. It makes more sense semantically
4. It should make the equivalence between pi_Lp and lp easier to implement

The new implementation of pi_Lp tries to retain as much as possible of the original implementation, while at the same time mimicking the implementation of lp. Many of the proofs are now significantly longer because of the required case splits.

• [x] depends on: #15852

---

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#15852~~ By Dependent Issues (🤖). Happy coding!

[bors[bot]]

:v: j-loreaux can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[j-loreaux]

bors r+

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

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