Commit 2022-08-16 04:11 e6f3561b

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.

• depends on: #15852