chore(analysis/mean_inequalities_pow): weaken assumptions on rpow_add…

…_le_rpow (#15823)

src/analysis/mean_inequalities_pow.lean

@@ -172,9 +172,11 @@ begin
   rwa one_div_div at h_rpow_add_rpow_le_add,
 end
 
-lemma rpow_add_le_add_rpow {p : ℝ} (a b : ℝ≥0) (hp_pos : 0 < p) (hp1 : p ≤ 1) :
+lemma rpow_add_le_add_rpow {p : ℝ} (a b : ℝ≥0) (hp : 0 ≤ p) (hp1 : p ≤ 1) :
   (a + b) ^ p ≤ a ^ p + b ^ p :=
 begin
+  rcases hp.eq_or_lt with rfl|hp_pos,
+  { simp },
   have h := rpow_add_rpow_le a b hp_pos hp1,
   rw one_div_one at h,
   repeat { rw nnreal.rpow_one at h },
@@ -286,9 +288,14 @@ begin
   rwa one_div_div at h_rpow_add_rpow_le_add,
 end
 
-lemma rpow_add_le_add_rpow {p : ℝ} (a b : ℝ≥0∞) (hp_pos : 0 < p) (hp1 : p ≤ 1) :
+lemma rpow_add_le_add_rpow {p : ℝ} (a b : ℝ≥0∞) (hp : 0 ≤ p) (hp1 : p ≤ 1) :
   (a + b) ^ p ≤ a ^ p + b ^ p :=
 begin
+  rcases hp.eq_or_lt with rfl|hp_pos,
+  { suffices : (1 : ℝ≥0∞) ≤ 1 + 1,
+    { simpa using this },
+    norm_cast,
+    norm_num },
   have h := rpow_add_rpow_le a b hp_pos hp1,
   rw one_div_one at h,
   repeat { rw ennreal.rpow_one at h },

src/analysis/normed_space/lp_space.lean

@@ -229,7 +229,7 @@ begin
   { refine (real.rpow_le_rpow (norm_nonneg _) (norm_add_le _ _) hp.le).trans _,
     dsimp [C],
     split_ifs with h h,
-    { simpa using nnreal.coe_le_coe.2 (nnreal.rpow_add_le_add_rpow (∥f i∥₊) (∥g i∥₊) hp h.le) },
+    { simpa using nnreal.coe_le_coe.2 (nnreal.rpow_add_le_add_rpow (∥f i∥₊) (∥g i∥₊) hp.le h.le) },
     { let F : fin 2 → ℝ≥0 := ![∥f i∥₊, ∥g i∥₊],
       have : ∀ i, (0:ℝ) ≤ F i := λ i, (F i).coe_nonneg,
       simp only [not_lt] at h,

src/measure_theory/function/lp_space.lean

@@ -760,7 +760,7 @@ end
 ... ≤ (∫⁻ a, (∥f a∥₊ : ℝ≥0∞) ^ q + (∥g a∥₊ : ℝ≥0∞) ^ q ∂μ) ^ (1 / q) :
 begin
   refine ennreal.rpow_le_rpow (lintegral_mono (λ a, _)) (by simp [hq_pos.le] : 0 ≤ 1 / q),
-  exact ennreal.rpow_add_le_add_rpow _ _ hq_pos hq1,
+  exact ennreal.rpow_add_le_add_rpow _ _ hq_pos.le hq1,
 end
 ... < ∞ :
 begin