mathlib

497b84d2 - chore(analysis/mean_inequalities): split integral mean inequalities to a new file (#7990)

chore(analysis/mean_inequalities): split integral mean inequalities to a new file (#7990) Currently, `normed_space.dual` imports a bunch of integration theory for no reason other than the file `mean_inequalities` contains both inequalities for finite sums and integrals. Splitting the file into two (and moving the integral versions to `measure_theory`) gives a more reasonable import graph.