mathlib3

68ced9a9 - chore(analysis/mean_inequalities_pow): nnreal versions of some ennreal inequalities (#10836)

chore(analysis/mean_inequalities_pow): nnreal versions of some ennreal inequalities (#10836) Make `nnreal` versions of the existing `ennreal` lemmas ```lean 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.