From 13bf7613c96a9fd66a81b9020a82cad9a6ea1fcf Mon Sep 17 00:00:00 2001
From: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Mon, 17 Apr 2023 16:24:10 +0000
Subject: [PATCH] feat(measure_theory/functions/lp_space): bounds on the sum of
 functions in L^p, p < 1, and applications (#18796)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The `L^p` space satisfies the triangular inequality for `p ≥ 1`. We show that, for `p < 1`, it satisfies a weaker inequality (with the loss of a multiplicative constant `2^(1/p - 1)`), which is still enough for several results. This makes it possible to remove the assumptions on `p` in results on density of continuous functions.
---
 src/analysis/mean_inequalities_pow.lean       |  36 ++++-
 .../function/continuous_map_dense.lean        | 119 ++++++--------
 src/measure_theory/function/lp_space.lean     | 152 ++++++++++++------
 .../function/simple_func_dense_lp.lean        | 106 +++++++-----
 .../integral/mean_inequalities.lean           |  23 +++
 5 files changed, 263 insertions(+), 173 deletions(-)

diff --git a/src/analysis/mean_inequalities_pow.lean b/src/analysis/mean_inequalities_pow.lean
index 57f964e83f40d..8292da30dfac0 100644
--- a/src/analysis/mean_inequalities_pow.lean
+++ b/src/analysis/mean_inequalities_pow.lean
@@ -109,6 +109,20 @@ begin
   { simp [hw', fin.sum_univ_succ], },
 end
 
+/-- Unweighted mean inequality, version for two elements of `ℝ≥0` and real exponents. -/
+theorem rpow_add_le_mul_rpow_add_rpow (z₁ z₂ : ℝ≥0) {p : ℝ} (hp : 1 ≤ p) :
+  (z₁ + z₂) ^ p ≤ 2^(p-1) * (z₁ ^ p + z₂ ^ p) :=
+begin
+  rcases eq_or_lt_of_le hp with rfl|h'p,
+  { simp only [rpow_one, sub_self, rpow_zero, one_mul] },
+  convert rpow_arith_mean_le_arith_mean2_rpow (1/2) (1/2) (2 * z₁) (2 * z₂) (add_halves 1) hp,
+  { simp only [one_div, inv_mul_cancel_left₀, ne.def, bit0_eq_zero, one_ne_zero, not_false_iff] },
+  { simp only [one_div, inv_mul_cancel_left₀, ne.def, bit0_eq_zero, one_ne_zero, not_false_iff] },
+  { have A : p - 1 ≠ 0 := ne_of_gt (sub_pos.2 h'p),
+    simp only [mul_rpow, rpow_sub' _ A, div_eq_inv_mul, rpow_one, mul_one],
+    ring }
+end
+
 /-- Weighted generalized mean inequality, version for sums over finite sets, with `ℝ≥0`-valued
 functions and real exponents. -/
 theorem arith_mean_le_rpow_mean (w z : ι → ℝ≥0) (hw' : ∑ i in s, w i = 1) {p : ℝ}
@@ -117,10 +131,6 @@ theorem arith_mean_le_rpow_mean (w z : ι → ℝ≥0) (hw' : ∑ i in s, w i =
 by exact_mod_cast real.arith_mean_le_rpow_mean s _ _ (λ i _, (w i).coe_nonneg)
   (by exact_mod_cast hw') (λ i _, (z i).coe_nonneg) hp
 
-end nnreal
-
-namespace nnreal
-
 private lemma add_rpow_le_one_of_add_le_one {p : ℝ} (a b : ℝ≥0) (hab : a + b ≤ 1)
   (hp1 : 1 ≤ p) :
   a ^ p + b ^ p ≤ 1 :=
@@ -248,9 +258,21 @@ begin
   { simp [hw', fin.sum_univ_succ], },
 end
 
-end ennreal
-
-namespace ennreal
+/-- Unweighted mean inequality, version for two elements of `ℝ≥0∞` and real exponents. -/
+theorem rpow_add_le_mul_rpow_add_rpow (z₁ z₂ : ℝ≥0∞) {p : ℝ} (hp : 1 ≤ p) :
+  (z₁ + z₂) ^ p ≤ 2^(p-1) * (z₁ ^ p + z₂ ^ p) :=
+begin
+  rcases eq_or_lt_of_le hp with rfl|h'p,
+  { simp only [rpow_one, sub_self, rpow_zero, one_mul, le_refl], },
+  convert rpow_arith_mean_le_arith_mean2_rpow
+    (1/2) (1/2) (2 * z₁) (2 * z₂) (ennreal.add_halves 1) hp,
+  { simp [← mul_assoc, ennreal.inv_mul_cancel two_ne_zero two_ne_top] },
+  { simp [← mul_assoc, ennreal.inv_mul_cancel two_ne_zero two_ne_top] },
+  { have A : p - 1 ≠ 0 := ne_of_gt (sub_pos.2 h'p),
+    simp only [mul_rpow_of_nonneg _ _ (zero_le_one.trans hp), rpow_sub _ _ two_ne_zero two_ne_top,
+      div_eq_inv_mul, rpow_one, mul_one],
+    ring }
+end
 
 lemma add_rpow_le_rpow_add {p : ℝ} (a b : ℝ≥0∞) (hp1 : 1 ≤ p) :
   a ^ p + b ^ p ≤ (a + b) ^ p :=
diff --git a/src/measure_theory/function/continuous_map_dense.lean b/src/measure_theory/function/continuous_map_dense.lean
index 8e8820280f4cc..f0d835f76c076 100644
--- a/src/measure_theory/function/continuous_map_dense.lean
+++ b/src/measure_theory/function/continuous_map_dense.lean
@@ -12,7 +12,7 @@ import measure_theory.integral.bochner
 /-!
 # Approximation in Lᵖ by continuous functions
 
-This file proves that bounded continuous functions are dense in `Lp E p μ`, for `1 ≤ p < ∞`, if the
+This file proves that bounded continuous functions are dense in `Lp E p μ`, for `p < ∞`, if the
 domain `α` of the functions is a normal topological space and the measure `μ` is weakly regular.
 It also proves the same results for approximation by continuous functions with compact support
 when the space is locally compact and `μ` is regular.
@@ -127,9 +127,9 @@ begin
 end
 
 /-- In a locally compact space, any function in `ℒp` can be approximated by compactly supported
-continuous functions when `1 ≤ p < ∞`, version in terms of `snorm`. -/
+continuous functions when `p < ∞`, version in terms of `snorm`. -/
 lemma mem_ℒp.exists_has_compact_support_snorm_sub_le
-  [locally_compact_space α] [μ.regular] (hp : p ≠ ∞) (h'p : 1 ≤ p)
+  [locally_compact_space α] [μ.regular] (hp : p ≠ ∞)
   {f : α → E} (hf : mem_ℒp f p μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
   ∃ (g : α → E), has_compact_support g ∧ snorm (f - g) p μ ≤ ε ∧ continuous g ∧ mem_ℒp g p μ :=
 begin
@@ -140,7 +140,7 @@ begin
   -- It suffices to check that the set of functions we consider approximates characteristic
   -- functions, is stable under addition and consists of ae strongly measurable functions.
   -- First check the latter easy facts.
-  apply hf.induction_dense hp h'p _ _ _ _ hε, rotate,
+  apply hf.induction_dense hp _ _ _ _ hε, rotate,
   -- stability under addition
   { rintros f g ⟨f_cont, f_mem, hf⟩ ⟨g_cont, g_mem, hg⟩,
     exact ⟨f_cont.add g_cont, f_mem.add g_mem, hf.add hg⟩ },
@@ -150,35 +150,26 @@ begin
   -- We are left with approximating characteristic functions.
   -- This follows from `exists_continuous_snorm_sub_le_of_closed`.
   assume c t ht htμ ε hε,
-  have h'ε : ε / 2 ≠ 0, by simpa using hε,
+  rcases exists_Lp_half E μ p hε with ⟨δ, δpos, hδ⟩,
   obtain ⟨η, ηpos, hη⟩ : ∃ (η : ℝ≥0), 0 < η ∧ ∀ (s : set α), μ s ≤ η →
-    snorm (s.indicator (λ x, c)) p μ ≤ ε / 2, from exists_snorm_indicator_le hp c h'ε,
+    snorm (s.indicator (λ x, c)) p μ ≤ δ, from exists_snorm_indicator_le hp c δpos.ne',
   have hη_pos' : (0 : ℝ≥0∞) < η, from ennreal.coe_pos.2 ηpos,
   obtain ⟨s, st, s_compact, μs⟩ : ∃ s ⊆ t, is_compact s ∧ μ (t \ s) < η,
     from ht.exists_is_compact_diff_lt htμ.ne hη_pos'.ne',
   have hsμ : μ s < ∞, from (measure_mono st).trans_lt htμ,
-  have I1 : snorm (s.indicator (λ y, c) - t.indicator (λ y, c)) p μ ≤ ε/2,
+  have I1 : snorm (s.indicator (λ y, c) - t.indicator (λ y, c)) p μ ≤ δ,
   { rw [← snorm_neg, neg_sub, ← indicator_diff st],
     exact (hη _ μs.le) },
   obtain ⟨k, k_compact, sk, -⟩ : ∃ (k : set α), is_compact k ∧ s ⊆ interior k ∧ k ⊆ univ,
     from exists_compact_between s_compact is_open_univ (subset_univ _),
   rcases exists_continuous_snorm_sub_le_of_closed hp s_compact.is_closed is_open_interior sk
-    hsμ.ne c h'ε with ⟨f, f_cont, I2, f_bound, f_support, f_mem⟩,
-  have I3 : snorm (f - t.indicator (λ y, c)) p μ ≤ ε, from calc
-    snorm (f - t.indicator (λ y, c)) p μ
-      = snorm ((f - s.indicator (λ y, c)) + (s.indicator (λ y, c) - t.indicator (λ y, c))) p μ :
-    by simp only [sub_add_sub_cancel]
-  ... ≤ snorm (f - s.indicator (λ y, c)) p μ
-        + snorm (s.indicator (λ y, c) - t.indicator (λ y, c)) p μ :
-    begin
-      refine snorm_add_le _ _ h'p,
-      { exact f_mem.ae_strongly_measurable.sub
-          (ae_strongly_measurable_const.indicator s_compact.measurable_set) },
-      { exact (ae_strongly_measurable_const.indicator s_compact.measurable_set).sub
-          (ae_strongly_measurable_const.indicator ht) },
-    end
-  ... ≤ ε/2 + ε/2 : add_le_add I2 I1
-  ... = ε : ennreal.add_halves _,
+    hsμ.ne c δpos.ne' with ⟨f, f_cont, I2, f_bound, f_support, f_mem⟩,
+  have I3 : snorm (f - t.indicator (λ y, c)) p μ ≤ ε,
+  { convert (hδ _ _ (f_mem.ae_strongly_measurable.sub
+        (ae_strongly_measurable_const.indicator s_compact.measurable_set))
+      ((ae_strongly_measurable_const.indicator s_compact.measurable_set).sub
+        (ae_strongly_measurable_const.indicator ht)) I2 I1).le,
+    simp only [sub_add_sub_cancel] },
   refine ⟨f, I3, f_cont, f_mem, has_compact_support.intro k_compact (λ x hx, _)⟩,
   rw ← function.nmem_support,
   contrapose! hx,
@@ -186,9 +177,9 @@ begin
 end
 
 /-- In a locally compact space, any function in `ℒp` can be approximated by compactly supported
-continuous functions when `1 ≤ p < ∞`, version in terms of `∫`. -/
+continuous functions when `0 < p < ∞`, version in terms of `∫`. -/
 lemma mem_ℒp.exists_has_compact_support_integral_rpow_sub_le
-  [locally_compact_space α] [μ.regular] {p : ℝ} (h'p : 1 ≤ p)
+  [locally_compact_space α] [μ.regular] {p : ℝ} (hp : 0 < p)
   {f : α → E} (hf : mem_ℒp f (ennreal.of_real p) μ) {ε : ℝ} (hε : 0 < ε) :
   ∃ (g : α → E), has_compact_support g ∧ ∫ x, ‖f x - g x‖^p ∂μ ≤ ε ∧ continuous g
     ∧ mem_ℒp g (ennreal.of_real p) μ :=
@@ -196,17 +187,15 @@ begin
   have I : 0 < ε ^ (1/p) := real.rpow_pos_of_pos hε _,
   have A : ennreal.of_real (ε ^ (1/p)) ≠ 0,
     by simp only [ne.def, ennreal.of_real_eq_zero, not_le, I],
-  have B : 1 ≤ ennreal.of_real p,
-  { convert ennreal.of_real_le_of_real h'p, exact ennreal.of_real_one.symm },
-  rcases hf.exists_has_compact_support_snorm_sub_le ennreal.coe_ne_top B A
+  have B : ennreal.of_real p ≠ 0, by simpa only [ne.def, ennreal.of_real_eq_zero, not_le] using hp,
+  rcases hf.exists_has_compact_support_snorm_sub_le ennreal.coe_ne_top A
     with ⟨g, g_support, hg, g_cont, g_mem⟩,
   change snorm _ (ennreal.of_real p) _ ≤ _ at hg,
   refine ⟨g, g_support, _, g_cont, g_mem⟩,
-  rwa [(hf.sub g_mem).snorm_eq_integral_rpow_norm (zero_lt_one.trans_le B).ne'
-    ennreal.coe_ne_top, ennreal.of_real_le_of_real_iff I.le, one_div,
-    ennreal.to_real_of_real (zero_le_one.trans h'p), real.rpow_le_rpow_iff _ hε.le _] at hg,
-  { exact integral_nonneg (λ x, real.rpow_nonneg_of_nonneg (norm_nonneg _) _) },
-  { exact inv_pos.2 (zero_lt_one.trans_le h'p) }
+  rwa [(hf.sub g_mem).snorm_eq_integral_rpow_norm B ennreal.coe_ne_top,
+    ennreal.of_real_le_of_real_iff I.le, one_div,
+    ennreal.to_real_of_real hp.le, real.rpow_le_rpow_iff _ hε.le (inv_pos.2 hp)] at hg,
+  exact integral_nonneg (λ x, real.rpow_nonneg_of_nonneg (norm_nonneg _) _),
 end
 
 /-- In a locally compact space, any integrable function can be approximated by compactly supported
@@ -217,7 +206,7 @@ lemma integrable.exists_has_compact_support_lintegral_sub_le [locally_compact_sp
     ∧ integrable g μ :=
 begin
   simp only [← mem_ℒp_one_iff_integrable, ← snorm_one_eq_lintegral_nnnorm] at hf ⊢,
-  exact hf.exists_has_compact_support_snorm_sub_le ennreal.one_ne_top le_rfl hε,
+  exact hf.exists_has_compact_support_snorm_sub_le ennreal.one_ne_top hε,
 end
 
 /-- In a locally compact space, any integrable function can be approximated by compactly supported
@@ -229,12 +218,12 @@ lemma integrable.exists_has_compact_support_integral_sub_le [locally_compact_spa
 begin
   simp only [← mem_ℒp_one_iff_integrable, ← snorm_one_eq_lintegral_nnnorm,
     ← ennreal.of_real_one] at hf ⊢,
-  simpa using hf.exists_has_compact_support_integral_rpow_sub_le le_rfl hε,
+  simpa using hf.exists_has_compact_support_integral_rpow_sub_le zero_lt_one hε,
 end
 
-/-- Any function in `ℒp` can be approximated by bounded continuous functions when `1 ≤ p < ∞`,
+/-- Any function in `ℒp` can be approximated by bounded continuous functions when `p < ∞`,
 version in terms of `snorm`. -/
-lemma mem_ℒp.exists_bounded_continuous_snorm_sub_le [μ.weakly_regular] (hp : p ≠ ∞) (h'p : 1 ≤ p)
+lemma mem_ℒp.exists_bounded_continuous_snorm_sub_le [μ.weakly_regular] (hp : p ≠ ∞)
   {f : α → E} (hf : mem_ℒp f p μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
   ∃ (g : α →ᵇ E), snorm (f - g) p μ ≤ ε ∧ mem_ℒp g p μ :=
 begin
@@ -245,7 +234,7 @@ begin
   -- It suffices to check that the set of functions we consider approximates characteristic
   -- functions, is stable under addition and made of ae strongly measurable functions.
   -- First check the latter easy facts.
-  apply hf.induction_dense hp h'p _ _ _ _ hε, rotate,
+  apply hf.induction_dense hp _ _ _ _ hε, rotate,
   -- stability under addition
   { rintros f g ⟨f_cont, f_mem, f_bd⟩ ⟨g_cont, g_mem, g_bd⟩,
     refine ⟨f_cont.add g_cont, f_mem.add g_mem, _⟩,
@@ -257,58 +246,46 @@ begin
   -- We are left with approximating characteristic functions.
   -- This follows from `exists_continuous_snorm_sub_le_of_closed`.
   assume c t ht htμ ε hε,
-  have h'ε : ε / 2 ≠ 0, by simpa using hε,
+  rcases exists_Lp_half E μ p hε with ⟨δ, δpos, hδ⟩,
   obtain ⟨η, ηpos, hη⟩ : ∃ (η : ℝ≥0), 0 < η ∧ ∀ (s : set α), μ s ≤ η →
-    snorm (s.indicator (λ x, c)) p μ ≤ ε / 2, from exists_snorm_indicator_le hp c h'ε,
+    snorm (s.indicator (λ x, c)) p μ ≤ δ, from exists_snorm_indicator_le hp c δpos.ne',
   have hη_pos' : (0 : ℝ≥0∞) < η, from ennreal.coe_pos.2 ηpos,
   obtain ⟨s, st, s_closed, μs⟩ : ∃ s ⊆ t, is_closed s ∧ μ (t \ s) < η,
     from ht.exists_is_closed_diff_lt htμ.ne hη_pos'.ne',
   have hsμ : μ s < ∞, from (measure_mono st).trans_lt htμ,
-  have I1 : snorm (s.indicator (λ y, c) - t.indicator (λ y, c)) p μ ≤ ε/2,
+  have I1 : snorm (s.indicator (λ y, c) - t.indicator (λ y, c)) p μ ≤ δ,
   { rw [← snorm_neg, neg_sub, ← indicator_diff st],
     exact (hη _ μs.le) },
   rcases exists_continuous_snorm_sub_le_of_closed hp s_closed is_open_univ (subset_univ _)
-    hsμ.ne c h'ε with ⟨f, f_cont, I2, f_bound, -, f_mem⟩,
-  have I3 : snorm (f - t.indicator (λ y, c)) p μ ≤ ε, from calc
-    snorm (f - t.indicator (λ y, c)) p μ
-      = snorm ((f - s.indicator (λ y, c)) + (s.indicator (λ y, c) - t.indicator (λ y, c))) p μ :
-    by simp only [sub_add_sub_cancel]
-  ... ≤ snorm (f - s.indicator (λ y, c)) p μ
-        + snorm (s.indicator (λ y, c) - t.indicator (λ y, c)) p μ :
-    begin
-      refine snorm_add_le _ _ h'p,
-      { exact f_mem.ae_strongly_measurable.sub
-          (ae_strongly_measurable_const.indicator s_closed.measurable_set) },
-      { exact (ae_strongly_measurable_const.indicator s_closed.measurable_set).sub
-          (ae_strongly_measurable_const.indicator ht) },
-    end
-  ... ≤ ε/2 + ε/2 : add_le_add I2 I1
-  ... = ε : ennreal.add_halves _,
+    hsμ.ne c δpos.ne' with ⟨f, f_cont, I2, f_bound, -, f_mem⟩,
+  have I3 : snorm (f - t.indicator (λ y, c)) p μ ≤ ε,
+  { convert (hδ _ _ (f_mem.ae_strongly_measurable.sub
+        (ae_strongly_measurable_const.indicator s_closed.measurable_set))
+      ((ae_strongly_measurable_const.indicator s_closed.measurable_set).sub
+        (ae_strongly_measurable_const.indicator ht)) I2 I1).le,
+    simp only [sub_add_sub_cancel] },
   refine ⟨f, I3, f_cont, f_mem, _⟩,
   exact (bounded_continuous_function.of_normed_add_comm_group f f_cont _ f_bound).bounded_range,
 end
 
-/-- Any function in `ℒp` can be approximated by bounded continuous functions when `1 ≤ p < ∞`,
+/-- Any function in `ℒp` can be approximated by bounded continuous functions when `0 < p < ∞`,
 version in terms of `∫`. -/
 lemma mem_ℒp.exists_bounded_continuous_integral_rpow_sub_le
-  [μ.weakly_regular] {p : ℝ} (h'p : 1 ≤ p)
+  [μ.weakly_regular] {p : ℝ} (hp : 0 < p)
   {f : α → E} (hf : mem_ℒp f (ennreal.of_real p) μ) {ε : ℝ} (hε : 0 < ε) :
   ∃ (g : α →ᵇ E), ∫ x, ‖f x - g x‖^p ∂μ ≤ ε ∧ mem_ℒp g (ennreal.of_real p) μ :=
 begin
   have I : 0 < ε ^ (1/p) := real.rpow_pos_of_pos hε _,
   have A : ennreal.of_real (ε ^ (1/p)) ≠ 0,
     by simp only [ne.def, ennreal.of_real_eq_zero, not_le, I],
-  have B : 1 ≤ ennreal.of_real p,
-  { convert ennreal.of_real_le_of_real h'p, exact ennreal.of_real_one.symm },
-  rcases hf.exists_bounded_continuous_snorm_sub_le ennreal.coe_ne_top B A
-    with ⟨g, hg, g_mem⟩,
+  have B : ennreal.of_real p ≠ 0, by simpa only [ne.def, ennreal.of_real_eq_zero, not_le] using hp,
+  rcases hf.exists_bounded_continuous_snorm_sub_le ennreal.coe_ne_top A with ⟨g, hg, g_mem⟩,
   change snorm _ (ennreal.of_real p) _ ≤ _ at hg,
   refine ⟨g, _, g_mem⟩,
-  rwa [(hf.sub g_mem).snorm_eq_integral_rpow_norm (zero_lt_one.trans_le B).ne'
-    ennreal.coe_ne_top, ennreal.of_real_le_of_real_iff I.le, one_div,
-    ennreal.to_real_of_real (zero_le_one.trans h'p), real.rpow_le_rpow_iff _ hε.le _] at hg,
-  { exact integral_nonneg (λ x, real.rpow_nonneg_of_nonneg (norm_nonneg _) _) },
-  { exact inv_pos.2 (zero_lt_one.trans_le h'p) }
+  rwa [(hf.sub g_mem).snorm_eq_integral_rpow_norm B ennreal.coe_ne_top,
+    ennreal.of_real_le_of_real_iff I.le, one_div,
+    ennreal.to_real_of_real hp.le, real.rpow_le_rpow_iff _ hε.le (inv_pos.2 hp)] at hg,
+  exact integral_nonneg (λ x, real.rpow_nonneg_of_nonneg (norm_nonneg _) _),
 end
 
 /-- Any integrable function can be approximated by bounded continuous functions,
@@ -318,7 +295,7 @@ lemma integrable.exists_bounded_continuous_lintegral_sub_le [μ.weakly_regular]
   ∃ (g : α →ᵇ E), ∫⁻ x, ‖f x - g x‖₊ ∂μ ≤ ε ∧ integrable g μ :=
 begin
   simp only [← mem_ℒp_one_iff_integrable, ← snorm_one_eq_lintegral_nnnorm] at hf ⊢,
-  exact hf.exists_bounded_continuous_snorm_sub_le ennreal.one_ne_top le_rfl hε,
+  exact hf.exists_bounded_continuous_snorm_sub_le ennreal.one_ne_top hε,
 end
 
 /-- Any integrable function can be approximated by bounded continuous functions,
@@ -329,7 +306,7 @@ lemma integrable.exists_bounded_continuous_integral_sub_le [μ.weakly_regular]
 begin
   simp only [← mem_ℒp_one_iff_integrable, ← snorm_one_eq_lintegral_nnnorm,
     ← ennreal.of_real_one] at hf ⊢,
-  simpa using hf.exists_bounded_continuous_integral_rpow_sub_le le_rfl hε,
+  simpa using hf.exists_bounded_continuous_integral_rpow_sub_le zero_lt_one hε,
 end
 
 namespace Lp
@@ -348,7 +325,7 @@ begin
   intros ε hε,
   have A : ennreal.of_real ε ≠ 0, by simp only [ne.def, ennreal.of_real_eq_zero, not_le, hε],
   obtain ⟨g, hg, g_mem⟩ : ∃ (g : α →ᵇ E), snorm (f - g) p μ ≤ ennreal.of_real ε ∧ mem_ℒp g p μ,
-    from (Lp.mem_ℒp f).exists_bounded_continuous_snorm_sub_le hp _i.out A,
+    from (Lp.mem_ℒp f).exists_bounded_continuous_snorm_sub_le hp A,
   refine ⟨g_mem.to_Lp _, _, ⟨g, rfl⟩⟩,
   simp only [dist_eq_norm, metric.mem_closed_ball'],
   rw Lp.norm_def,
diff --git a/src/measure_theory/function/lp_space.lean b/src/measure_theory/function/lp_space.lean
index ab45f937e1a84..851f9dc88bdf9 100644
--- a/src/measure_theory/function/lp_space.lean
+++ b/src/measure_theory/function/lp_space.lean
@@ -706,6 +706,20 @@ end
 ... ≤ snorm' f q μ + snorm' g q μ :
   ennreal.lintegral_Lp_add_le hf.ennnorm hg.ennnorm hq1
 
+lemma snorm'_add_le_of_le_one {f g : α → E}
+  (hf : ae_strongly_measurable f μ) (hq0 : 0 ≤ q) (hq1 : q ≤ 1) :
+  snorm' (f + g) q μ ≤ 2^(1/q-1) * (snorm' f q μ + snorm' g q μ) :=
+calc (∫⁻ a, ↑‖(f + g) a‖₊ ^ q ∂μ) ^ (1 / q)
+    ≤ (∫⁻ a, (((λ a, (‖f a‖₊ : ℝ≥0∞))
+        + (λ a, (‖g a‖₊ : ℝ≥0∞))) a) ^ q ∂μ) ^ (1 / q) :
+begin
+  refine ennreal.rpow_le_rpow _ (by simp [hq0] : 0 ≤ 1 / q),
+  refine lintegral_mono (λ a, ennreal.rpow_le_rpow _ hq0),
+  simp [←ennreal.coe_add, nnnorm_add_le],
+end
+... ≤ 2^(1/q-1) * (snorm' f q μ + snorm' g q μ) :
+  ennreal.lintegral_Lp_add_le_of_le_one hf.ennnorm hq0 hq1
+
 lemma snorm_ess_sup_add_le {f g : α → F} :
   snorm_ess_sup (f + g) μ ≤ snorm_ess_sup f μ + snorm_ess_sup g μ :=
 begin
@@ -729,9 +743,78 @@ begin
   exact snorm'_add_le hf hg hp1_real,
 end
 
-lemma snorm_sub_le
-  {f g : α → E} (hf : ae_strongly_measurable f μ) (hg : ae_strongly_measurable g μ) (hp1 : 1 ≤ p) :
-  snorm (f - g) p μ ≤ snorm f p μ + snorm g p μ :=
+/-- A constant for the inequality `‖f + g‖_{L^p} ≤ C * (‖f‖_{L^p} + ‖g‖_{L^p})`. It is equal to `1`
+for `p ≥ 1` or `p = 0`, and `2^(1/p-1)` in the more tricky interval `(0, 1)`. -/
+def Lp_add_const (p : ℝ≥0∞) : ℝ≥0∞ :=
+if p ∈ set.Ioo (0 : ℝ≥0∞) 1 then 2^(1/p.to_real-1) else 1
+
+lemma Lp_add_const_of_one_le {p : ℝ≥0∞} (hp : 1 ≤ p) : Lp_add_const p = 1 :=
+begin
+  rw [Lp_add_const, if_neg],
+  assume h,
+  exact lt_irrefl _ (h.2.trans_le hp),
+end
+
+lemma Lp_add_const_zero : Lp_add_const 0 = 1 :=
+begin
+  rw [Lp_add_const, if_neg],
+  assume h,
+  exact lt_irrefl _ (h.1),
+end
+
+lemma Lp_add_const_lt_top (p : ℝ≥0∞) : Lp_add_const p < ∞ :=
+begin
+  rw [Lp_add_const],
+  split_ifs,
+  { apply ennreal.rpow_lt_top_of_nonneg _ ennreal.two_ne_top,
+    simp only [one_div, sub_nonneg],
+    apply one_le_inv (ennreal.to_real_pos h.1.ne' (h.2.trans ennreal.one_lt_top).ne),
+    simpa using ennreal.to_real_mono ennreal.one_ne_top h.2.le },
+  { exact ennreal.one_lt_top }
+end
+
+lemma snorm_add_le'
+  {f g : α → E} (hf : ae_strongly_measurable f μ) (hg : ae_strongly_measurable g μ) (p : ℝ≥0∞) :
+  snorm (f + g) p μ ≤ Lp_add_const p * (snorm f p μ + snorm g p μ) :=
+begin
+  rcases eq_or_ne p 0 with rfl|hp,
+  { simp only [snorm_exponent_zero, add_zero, mul_zero, le_zero_iff] },
+  rcases lt_or_le p 1 with h'p|h'p,
+  { simp only [snorm_eq_snorm' hp (h'p.trans ennreal.one_lt_top).ne],
+    convert snorm'_add_le_of_le_one hf ennreal.to_real_nonneg _,
+    { have : p ∈ set.Ioo (0 : ℝ≥0∞) 1 := ⟨hp.bot_lt, h'p⟩,
+      simp only [Lp_add_const, if_pos this] },
+    { simpa using ennreal.to_real_mono ennreal.one_ne_top h'p.le } },
+  { simp [Lp_add_const_of_one_le h'p],
+    exact snorm_add_le hf hg h'p }
+end
+
+variables (μ E)
+/-- Technical lemma to control the addition of functions in `L^p` even for `p < 1`: Given `δ > 0`,
+there exists `η` such that two functions bounded by `η` in `L^p` have a sum bounded by `δ`. One
+could take `η = δ / 2` for `p ≥ 1`, but the point of the lemma is that it works also for `p < 1`.
+-/
+lemma exists_Lp_half (p : ℝ≥0∞) {δ : ℝ≥0∞} (hδ : δ ≠ 0) :
+  ∃ (η : ℝ≥0∞), 0 < η ∧ ∀ (f g : α → E) (hf : ae_strongly_measurable f μ)
+    (hg : ae_strongly_measurable g μ) (Hf : snorm f p μ ≤ η) (Hg : snorm g p μ ≤ η),
+      snorm (f + g) p μ < δ :=
+begin
+  have : tendsto (λ (η : ℝ≥0∞), Lp_add_const p * (η + η)) (𝓝[>] 0) (𝓝 (Lp_add_const p * (0 + 0))),
+    from (ennreal.tendsto.const_mul (tendsto_id.add tendsto_id)
+      (or.inr (Lp_add_const_lt_top p).ne)).mono_left nhds_within_le_nhds,
+  simp only [add_zero, mul_zero] at this,
+  rcases (((tendsto_order.1 this).2 δ hδ.bot_lt).and self_mem_nhds_within).exists
+    with ⟨η, hη, ηpos⟩,
+  refine ⟨η, ηpos, λ f g hf hg Hf Hg, _⟩,
+  calc snorm (f + g) p μ ≤ Lp_add_const p * (snorm f p μ + snorm g p μ) : snorm_add_le' hf hg p
+  ... ≤ Lp_add_const p * (η + η) : mul_le_mul_of_nonneg_left (add_le_add Hf Hg) bot_le
+  ... < δ : hη
+end
+variables {μ E}
+
+lemma snorm_sub_le'
+  {f g : α → E} (hf : ae_strongly_measurable f μ) (hg : ae_strongly_measurable g μ) (p : ℝ≥0∞) :
+  snorm (f - g) p μ ≤ Lp_add_const p * (snorm f p μ + snorm g p μ) :=
 calc snorm (f - g) p μ = snorm (f + - g) p μ : by rw sub_eq_add_neg
   -- We cannot use snorm_add_le on f and (-g) because we don't have `ae_measurable (-g) μ`, since
   -- we don't suppose `[borel_space E]`.
@@ -739,55 +822,23 @@ calc snorm (f - g) p μ = snorm (f + - g) p μ : by rw sub_eq_add_neg
 ... ≤ snorm (λ x, ‖f x‖ + ‖- g x‖) p μ : by
 { refine snorm_mono_real (λ x, _), rw norm_norm, exact norm_add_le _ _, }
 ... = snorm (λ x, ‖f x‖ + ‖g x‖) p μ : by simp_rw norm_neg
-... ≤ snorm (λ x, ‖f x‖) p μ + snorm (λ x, ‖g x‖) p μ : snorm_add_le hf.norm hg.norm hp1
-... = snorm f p μ + snorm g p μ : by rw [← snorm_norm f, ← snorm_norm g]
-
-lemma snorm_add_lt_top_of_one_le {f g : α → E} (hf : mem_ℒp f p μ) (hg : mem_ℒp g p μ)
-  (hq1 : 1 ≤ p) : snorm (f + g) p μ < ∞ :=
-lt_of_le_of_lt (snorm_add_le hf.1 hg.1 hq1) (ennreal.add_lt_top.mpr ⟨hf.2, hg.2⟩)
+... ≤ Lp_add_const p * (snorm (λ x, ‖f x‖) p μ + snorm (λ x, ‖g x‖) p μ) :
+  snorm_add_le' hf.norm hg.norm p
+... = Lp_add_const p * (snorm f p μ + snorm g p μ) : by rw [← snorm_norm f, ← snorm_norm g]
 
-lemma snorm'_add_lt_top_of_le_one
-  {f g : α → E} (hf : ae_strongly_measurable f μ)
-  (hf_snorm : snorm' f q μ < ∞) (hg_snorm : snorm' g q μ < ∞) (hq_pos : 0 < q) (hq1 : q ≤ 1) :
-  snorm' (f + g) q μ < ∞ :=
-calc (∫⁻ a, ↑‖(f + g) a‖₊ ^ q ∂μ) ^ (1 / q)
-    ≤ (∫⁻ a, (((λ a, (‖f a‖₊ : ℝ≥0∞))
-        + (λ a, (‖g a‖₊ : ℝ≥0∞))) a) ^ q ∂μ) ^ (1 / q) :
-begin
-  refine ennreal.rpow_le_rpow _ (by simp [hq_pos.le] : 0 ≤ 1 / q),
-  refine lintegral_mono (λ a, ennreal.rpow_le_rpow _ hq_pos.le),
-  simp [←ennreal.coe_add, nnnorm_add_le],
-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.le hq1,
-end
-... < ∞ :
-begin
-  refine ennreal.rpow_lt_top_of_nonneg (by simp [hq_pos.le] : 0 ≤ 1 / q) _,
-  rw [lintegral_add_left' (hf.ennnorm.pow_const q), ennreal.add_ne_top],
-  exact ⟨(lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top hq_pos hf_snorm).ne,
-    (lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top hq_pos hg_snorm).ne⟩,
-end
+lemma snorm_sub_le
+  {f g : α → E} (hf : ae_strongly_measurable f μ) (hg : ae_strongly_measurable g μ) (hp : 1 ≤ p) :
+  snorm (f - g) p μ ≤ snorm f p μ + snorm g p μ :=
+by simpa [Lp_add_const_of_one_le hp] using snorm_sub_le' hf hg p
 
 lemma snorm_add_lt_top {f g : α → E} (hf : mem_ℒp f p μ) (hg : mem_ℒp g p μ) :
-  snorm (f + g) p μ < ∞ :=
+  snorm (f + g) p μ < ∞ := calc
+snorm (f + g) p μ ≤ Lp_add_const p * (snorm f p μ + snorm g p μ) :
+  snorm_add_le' hf.ae_strongly_measurable hg.ae_strongly_measurable p
+... < ∞ :
 begin
-  by_cases h0 : p = 0,
-  { simp [h0], },
-  rw ←ne.def at h0,
-  cases le_total 1 p with hp1 hp1,
-  { exact snorm_add_lt_top_of_one_le hf hg hp1, },
-  have hp_top : p ≠ ∞, from (lt_of_le_of_lt hp1 ennreal.coe_lt_top).ne,
-  have hp_pos : 0 < p.to_real,
-  { rw [← ennreal.zero_to_real, @ennreal.to_real_lt_to_real 0 p ennreal.coe_ne_top hp_top],
-    exact ((zero_le p).lt_of_ne h0.symm), },
-  have hp1_real : p.to_real ≤ 1,
-  { rwa [← ennreal.one_to_real, @ennreal.to_real_le_to_real p 1 hp_top ennreal.coe_ne_top], },
-  rw snorm_eq_snorm' h0 hp_top,
-  rw [mem_ℒp, snorm_eq_snorm' h0 hp_top] at hf hg,
-  exact snorm'_add_lt_top_of_le_one hf.1 hf.2 hg.2 hp_pos hp1_real,
+  apply ennreal.mul_lt_top (Lp_add_const_lt_top p).ne,
+  exact ((ennreal.add_lt_top).2 ⟨hf.2, hg.2⟩).ne,
 end
 
 section map_measure
@@ -918,9 +969,6 @@ begin
   simp [snorm_eq_snorm' h0 h_top],
 end
 
-section borel_space
--- variable [borel_space E]
-
 lemma mem_ℒp.neg {f : α → E} (hf : mem_ℒp f p μ) : mem_ℒp (-f) p μ :=
 ⟨ae_strongly_measurable.neg hf.1, by simp [hf.right]⟩
 
@@ -1160,8 +1208,6 @@ end
 
 end has_measurable_add
 
-end borel_space
-
 section normed_space
 
 variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F]
diff --git a/src/measure_theory/function/simple_func_dense_lp.lean b/src/measure_theory/function/simple_func_dense_lp.lean
index b8a92f376fba8..1853843cf77f6 100644
--- a/src/measure_theory/function/simple_func_dense_lp.lean
+++ b/src/measure_theory/function/simple_func_dense_lp.lean
@@ -186,6 +186,31 @@ lemma tendsto_approx_on_range_Lp [borel_space E]
 by simpa only [Lp.tendsto_Lp_iff_tendsto_ℒp'']
   using tendsto_approx_on_range_Lp_snorm hp_ne_top fmeas hf.2
 
+/-- Any function in `ℒp` can be approximated by a simple function if `p < ∞`. -/
+lemma _root_.measure_theory.mem_ℒp.exists_simple_func_snorm_sub_lt
+  {E : Type*} [normed_add_comm_group E]
+  {f : β → E} {μ : measure β} (hf : mem_ℒp f p μ) (hp_ne_top : p ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
+  ∃ (g : β →ₛ E), snorm (f - g) p μ < ε ∧ mem_ℒp g p μ :=
+begin
+  borelize E,
+  let f' := hf.1.mk f,
+  suffices H : ∃ (g : β →ₛ E), snorm (f' - g) p μ < ε ∧ mem_ℒp g p μ,
+  { rcases H with ⟨g, hg, g_mem⟩,
+    refine ⟨g, _, g_mem⟩,
+    convert hg using 1,
+    apply snorm_congr_ae,
+    filter_upwards [hf.1.ae_eq_mk] with x hx,
+    simpa only [pi.sub_apply, sub_left_inj] using hx },
+  have hf' : mem_ℒp f' p μ, from hf.ae_eq hf.1.ae_eq_mk,
+  have f'meas : measurable f' := hf.1.measurable_mk,
+  haveI : separable_space (range f' ∪ {0} : set E),
+    from strongly_measurable.separable_space_range_union_singleton hf.1.strongly_measurable_mk,
+  rcases ((tendsto_order.1 (tendsto_approx_on_range_Lp_snorm hp_ne_top f'meas hf'.2)).2
+    ε hε.bot_lt).exists with ⟨n, hn⟩,
+  rw [← snorm_neg, neg_sub] at hn,
+  exact ⟨_, hn, mem_ℒp_approx_on_range f'meas hf' _⟩,
+end
+
 end Lp
 
 /-! ### L1 approximation by simple functions -/
@@ -897,7 +922,7 @@ end
 
 /-- If a set of ae strongly measurable functions is stable under addition and approximates
 characteristic functions in `ℒp`, then it is dense in `ℒp`. -/
-lemma mem_ℒp.induction_dense (hp_ne_top : p ≠ ∞) (h'p : 1 ≤ p) (P : (α → E) → Prop)
+lemma mem_ℒp.induction_dense (hp_ne_top : p ≠ ∞) (P : (α → E) → Prop)
   (h0P : ∀ (c : E) ⦃s : set α⦄, measurable_set s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 →
     (∃ (g : α → E), snorm (g - s.indicator (λ x, c)) p μ ≤ ε ∧ P g))
   (h1P : ∀ f g, P f → P g → P (f + g))
@@ -905,48 +930,45 @@ lemma mem_ℒp.induction_dense (hp_ne_top : p ≠ ∞) (h'p : 1 ≤ p) (P : (α
   {f : α → E} (hf : mem_ℒp f p μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
   ∃ (g : α → E), snorm (f - g) p μ ≤ ε ∧ P g :=
 begin
-  haveI : fact (1 ≤ p) := ⟨h'p⟩,
-  revert f hf ε,
-  refine mem_ℒp.induction hp_ne_top _ _ _ _ _,
-  { assume c s hs hμs ε εpos,
-    rcases h0P c hs hμs εpos with ⟨g, hg, Pg⟩,
-    rw [← snorm_neg, neg_sub] at hg,
-    exact ⟨g, hg, Pg⟩ },
-  { assume f f' hff' hf hf' Hf Hf' ε εpos,
-    have A : ε / 2 ≠ 0, by simp [εpos],
-    rcases Hf A with ⟨g, hfg, Pg⟩,
-    rcases Hf' A with ⟨g', hf'g', Pg'⟩,
-    refine ⟨g + g', _, h1P g g' Pg Pg'⟩,
-    calc snorm (f + f' - (g + g')) p μ
-        = snorm ((f - g) + (f' - g')) p μ : by { congr' 1, abel }
-    ... ≤ snorm (f - g) p μ + snorm (f' - g') p μ :
-      snorm_add_le (hf.ae_strongly_measurable.sub (h2P g Pg))
-        (hf'.ae_strongly_measurable.sub (h2P g' Pg')) h'p
-    ... ≤ ε / 2 + ε / 2 : add_le_add hfg hf'g'
-    ... = ε : ennreal.add_halves _ },
-  { rw is_closed_iff_nhds,
-    assume f hf ε εpos,
-    have A : ε / 2 ≠ 0, by simp [εpos],
-    rcases hf (emetric.ball f (ε/2)) (emetric.ball_mem_nhds _ A.bot_lt) with ⟨f', hf', h'f'⟩,
-    rcases h'f' A with ⟨g, hg, Pg⟩,
-    refine ⟨g, _, Pg⟩,
-    calc snorm (f - g) p μ = snorm ((f - f') + (f' - g)) p μ : by simp only [sub_add_sub_cancel]
-    ... ≤ snorm (f - f') p μ + snorm (f' - g) p μ :
-      snorm_add_le ((Lp.mem_ℒp f).sub (Lp.mem_ℒp f')).ae_strongly_measurable
-        ((Lp.mem_ℒp f').ae_strongly_measurable.sub (h2P g Pg)) h'p
-    ... ≤ ε / 2 + ε / 2 :
-      begin
-        refine add_le_add _ hg,
-        rw [← snorm_neg, neg_sub],
-        simp only [Lp.edist_def, emetric.mem_ball] at hf',
-        exact hf'.le
-      end
-    ... = ε : ennreal.add_halves _ },
-  { assume f f' hff' hf Hf ε εpos,
-    rcases Hf εpos with ⟨g, hg, Pg⟩,
+  rcases eq_or_ne p 0 with rfl|hp_pos,
+  { rcases h0P (0 : E) measurable_set.empty
+      (by simp only [measure_empty, with_top.zero_lt_top]) hε with ⟨g, hg, Pg⟩,
+    exact ⟨g, by simp only [snorm_exponent_zero, zero_le'], Pg⟩ },
+  suffices H : ∀ (f' : α →ₛ E) (δ : ℝ≥0∞) (hδ : δ ≠ 0), mem_ℒp f' p μ →
+    ∃ g, snorm (f' - g) p μ ≤ δ ∧ P g,
+  { obtain ⟨η, ηpos, hη⟩ := exists_Lp_half E μ p hε,
+    rcases hf.exists_simple_func_snorm_sub_lt hp_ne_top ηpos.ne' with ⟨f', hf', f'_mem⟩,
+    rcases H f' η ηpos.ne' f'_mem with ⟨g, hg, Pg⟩,
     refine ⟨g, _, Pg⟩,
-    have : f - g =ᵐ[μ] f' - g := hff'.sub (filter.germ.coe_eq.mp rfl),
-    rwa ← snorm_congr_ae this }
+    convert (hη _ _ (hf.ae_strongly_measurable.sub f'.ae_strongly_measurable)
+      (f'.ae_strongly_measurable.sub (h2P g Pg)) hf'.le hg).le,
+    simp only [sub_add_sub_cancel] },
+  refine simple_func.induction _ _,
+  { intros c s hs ε εpos Hs,
+    rcases eq_or_ne c 0 with rfl|hc,
+    { rcases h0P (0 : E) measurable_set.empty
+        (by simp only [measure_empty, with_top.zero_lt_top]) εpos with ⟨g, hg, Pg⟩,
+      rw [← snorm_neg, neg_sub] at hg,
+      refine ⟨g, _, Pg⟩,
+      convert hg,
+      ext x,
+      simp only [simple_func.const_zero, simple_func.coe_piecewise, simple_func.coe_zero,
+        piecewise_eq_indicator, indicator_zero', pi.zero_apply, indicator_zero] },
+    { have : μ s < ∞,
+        from (simple_func.measure_lt_top_of_mem_ℒp_indicator hp_pos hp_ne_top hc hs Hs),
+      rcases h0P c hs this εpos with ⟨g, hg, Pg⟩,
+      rw [← snorm_neg, neg_sub] at hg,
+      exact ⟨g, hg, Pg⟩ } },
+  { intros f f' hff' hf hf' δ δpos int_ff',
+    obtain ⟨η, ηpos, hη⟩ := exists_Lp_half E μ p δpos,
+    rw [simple_func.coe_add,
+      mem_ℒp_add_of_disjoint hff' f.strongly_measurable f'.strongly_measurable] at int_ff',
+    rcases hf η ηpos.ne' int_ff'.1 with ⟨g, hg, Pg⟩,
+    rcases hf' η ηpos.ne' int_ff'.2 with ⟨g', hg', Pg'⟩,
+    refine ⟨g + g', _, h1P g g' Pg Pg'⟩,
+    convert (hη _ _ (f.ae_strongly_measurable.sub (h2P g Pg))
+          (f'.ae_strongly_measurable.sub (h2P g' Pg')) hg hg').le,
+    abel }
 end
 
 section integrable
diff --git a/src/measure_theory/integral/mean_inequalities.lean b/src/measure_theory/integral/mean_inequalities.lean
index 9c902c4f1671a..9c8942b2eba36 100644
--- a/src/measure_theory/integral/mean_inequalities.lean
+++ b/src/measure_theory/integral/mean_inequalities.lean
@@ -377,6 +377,29 @@ begin
   exact lintegral_Lp_add_le_aux hpq hf hf_top hg hg_top h0 htop,
 end
 
+/-- Variant of Minkowski's inequality for functions `α → ℝ≥0∞` in `ℒp` with `p ≤ 1`: the `ℒp`
+seminorm of the sum of two functions is bounded by a constant multiple of the sum
+of their `ℒp` seminorms. -/
+theorem lintegral_Lp_add_le_of_le_one {p : ℝ} {f g : α → ℝ≥0∞}
+  (hf : ae_measurable f μ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) :
+  (∫⁻ a, ((f + g) a)^p ∂ μ) ^ (1/p) ≤
+    2^(1/p-1) * ((∫⁻ a, (f a)^p ∂μ) ^ (1/p) + (∫⁻ a, (g a)^p ∂μ) ^ (1/p)) :=
+begin
+  rcases eq_or_lt_of_le hp0 with rfl|hp,
+  { simp only [pi.add_apply, rpow_zero, lintegral_one, _root_.div_zero, zero_sub],
+    norm_num,
+    rw [rpow_neg, rpow_one, ennreal.inv_mul_cancel two_ne_zero two_ne_top],
+    exact le_rfl },
+  calc (∫⁻ a, (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ a, (f a)^p ∂ μ + ∫⁻ a, (g a)^p ∂ μ) ^ (1/p) :
+    begin
+      apply rpow_le_rpow _ (div_nonneg zero_le_one hp0),
+      rw ← lintegral_add_left' (hf.pow_const p),
+      exact lintegral_mono (λ a, rpow_add_le_add_rpow _ _ hp0 hp1)
+    end
+  ... ≤ 2 ^ (1/p-1) * ((∫⁻ a, f a ^ p ∂μ) ^ (1/p) + (∫⁻ a, g a ^ p ∂μ) ^ (1/p)) :
+    rpow_add_le_mul_rpow_add_rpow _ _ ((one_le_div hp).2 hp1)
+end
+
 end ennreal
 
 /-- Hölder's inequality for functions `α → ℝ≥0`. The integral of the product of two functions