mathlib3

49e50ee5 - feat(measure_theory/lp_space): add more API on Lp spaces (#6042)

feat(measure_theory/lp_space): add more API on Lp spaces (#6042) Flesh out the file on `L^p` spaces, notably adding facts on the composition with Lipschitz functions. This makes it possible to define in one go the positive part of an `L^p` function, and its image under a continuous linear map. The file `ae_eq_fun.lean` is split into two, to solve a temporary issue: this file defines a global emetric space instance (of `L^1` type) on the space of function classes. This passes to subtypes, and clashes with the topology on `L^p` coming from the distance. This did not show up before as there were not enough topological statements on `L^p`, but I have been bitten by this when adding new results. For now, we move this part of `ae_eq_fun.lean` to another file which is not imported by `lp_space.lean`, to avoid the clash. This will be solved in a subsequent PR in which I will remove the global instance, and construct the integral based on the specialization of `L^p` to `p = 1` instead of the ad hoc construction we have now (note that, currently, we have two different `L^1` spaces in mathlib, denoted `Lp E 1 μ` and `α →₁[μ] E` -- I will remove the second one in a later PR). Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>