Commit 2021-12-16 09:07 68ced9a9

chore(analysis/mean_inequalities_pow): nnreal versions of some ennreal inequalities (#10836) Make nnreal versions of the existing ennreal lemmas

lemma add_rpow_le_rpow_add {p : ℝ} (a b : ℝ≥0∞) (hp1 : 1 ≤ p) :
  a ^ p + b ^ p ≤ (a + b) ^ p 

and similar, introduced by @RemyDegenne in #5828. Refactor the proofs of the ennreal versions to pass through these.