[Merged by Bors] - chore(analysis/mean_inequalities): split integral mean inequalities to a new file

[sgouezel]

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.

---

no math changes at all

[hrmacbeth]

If I understand correctly, the analysis.special_functions.* files still import the beginning of measure theory (see import measure_theory.borel_space in analysis.special_functions.exp_log).

Are you planning to let this remain (so the point of the PR is to reduce the size of the measure theory import to mean_inequalities rather than eliminate it entirely)? We could get rid of the measure theory import completely if the measurabilty results moved to analysis.special_functions.integrals.

By the way, another possible improvement to the import graph would be to remove the inner_product_space theorems (i.e., Riesz representation theorem) from normed_space.dual and put them in analysis.normed_space.inner_product.

[sgouezel]

You're absolutely right that there is more to do to disentangle the imports. This PR is just one part of it, I'll probably go on improving the situation once this is merged.

[PatrickMassot]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests