Commit 2020-11-14 18:20 9b887d51

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] -->