Commit 2021-11-17 09:02 d5c2b34c

chore(analysis/mean_inequalities): split mean_inequalities into two files (#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.