Commit 2021-06-19 15:31 497b84d2

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.