feat(measure_theory/lp_space): Define Lp spaces (#4993)
Define the space Lp of functions for which the norm raised to the power p has finite integral.
Define the seminorm on that space (without proof that it is a seminorm, for now).
Add three lemmas to analysis/special_functions/pow.lean about ennreal.rpow
<!--
put comments you want to keep out of the PR commit here.
If this PR depends on other PRs, please list them below this comment,
using the following format:
- [ ] depends on: #abc [optional extra text]
- [ ] depends on: #xyz [optional extra text]
-->
