chore(analysis/mean_inequalities): split mean_inequalities into two f…

…iles (#10355)

This PR puts all results related to power functions into a new file.

Currently, we prove convexity of `exp` and `pow`, then use those properties in `mean_inequalities`. I am refactoring some parts of the analysis library to reduce the use of derivatives. I want to prove convexity of exp without derivatives (in a future PR), prove Holder's inequality, then use it to prove the convexity of pow. This requires Holder's inequality to be in a file that does not use convexity of pow, hence the split.

I needed to change the proof of Holder's inequality since it used the generalized mean inequality (hence `pow`). I switched to the second possible proof mentioned in the file docstring.

I also moved some lemmas in `mean_inequalities` to have three main sections: AM-GM, then Young and a final section with Holder and Minkowski.