mathlib3

41191815 - feat(measure_theory/l2_space): L2 is an inner product space (#6596)

feat(measure_theory/l2_space): L2 is an inner product space (#6596) If `E` is an inner product space, then so is `Lp E 2 µ`, with inner product being the integral of the inner products between function values. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>