mathlib

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

refactor(analysis/normed_space/pi_Lp): make argument of pi_Lp a term of ℝ≥0∞ instead of ℝ (#15833) 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