feat(analysis/mean_inequalities, measure_theory/lp_space): extend mem…

…_Lp.add to all p in ennreal (#5828)

Show `(a ^ q + b ^ q) ^ (1/q) ≤ (a ^ p + b ^ p) ^ (1/p)` for `a,b : ennreal` and `0 < p <= q`.

Use it to show that for `p <= 1`, if measurable functions `f` and `g` are in Lp, `f+g` is also in Lp (the case `1 <= p` is already done).

src/analysis/mean_inequalities.lean

@@ -600,6 +600,71 @@ begin
   { apply finset.sum_congr rfl (λ i hi, _), simp [H'.1 i hi, H'.2 i hi] }
 end
 
+private lemma add_rpow_le_one_of_add_le_one {p : ℝ} (a b : ennreal) (hab : a + b ≤ 1)
+  (hp1 : 1 ≤ p) :
+  a ^ p + b ^ p ≤ 1 :=
+begin
+  have h_le_one : ∀ x : ennreal, x ≤ 1 → x ^ p ≤ x, from λ x hx, rpow_le_self_of_le_one hx hp1,
+  have ha : a ≤ 1, from (self_le_add_right a b).trans hab,
+  have hb : b ≤ 1, from (self_le_add_left b a).trans hab,
+  exact (add_le_add (h_le_one a ha) (h_le_one b hb)).trans hab,
+end
+
+lemma add_rpow_le_rpow_add {p : ℝ} (a b : ennreal) (hp1 : 1 ≤ p) :
+  a ^ p + b ^ p ≤ (a + b) ^ p :=
+begin
+  have hp_pos : 0 < p := lt_of_lt_of_le zero_lt_one hp1,
+  by_cases h_top : a + b = ⊤,
+  { rw ←@ennreal.rpow_eq_top_iff_of_pos (a + b) p hp_pos at h_top,
+    rw h_top,
+    exact le_top, },
+  obtain ⟨ha_top, hb_top⟩ := add_ne_top.mp h_top,
+  by_cases h_zero : a + b = 0,
+  { simp [add_eq_zero_iff.mp h_zero, ennreal.zero_rpow_of_pos hp_pos], },
+  have h_nonzero : ¬(a = 0 ∧ b = 0), by rwa add_eq_zero_iff at h_zero,
+  have h_add : a/(a+b) + b/(a+b) = 1, by rw [div_add_div_same, div_self h_zero h_top],
+  have h := add_rpow_le_one_of_add_le_one (a/(a+b)) (b/(a+b)) h_add.le hp1,
+  rw [div_rpow_of_nonneg a (a+b) hp_pos.le, div_rpow_of_nonneg b (a+b) hp_pos.le] at h,
+  have hab_0 : (a + b)^p ≠ 0, by simp [ha_top, hb_top, hp_pos, h_nonzero],
+  have hab_top : (a + b)^p ≠ ⊤, by simp [ha_top, hb_top, hp_pos, h_nonzero],
+  have h_mul : (a + b)^p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b)^p,
+  { nth_rewrite 3 ←mul_one ((a + b)^p),
+    exact (mul_le_mul_left hab_0 hab_top).mpr h, },
+  rwa [div_eq_mul_inv, div_eq_mul_inv, mul_add, mul_comm (a^p), mul_comm (b^p), ←mul_assoc,
+    ←mul_assoc, mul_inv_cancel hab_0 hab_top, one_mul, one_mul] at h_mul,
+end
+
+lemma rpow_add_rpow_le_add {p : ℝ} (a b : ennreal) (hp1 : 1 ≤ p) :
+  (a ^ p + b ^ p) ^ (1/p) ≤ a + b :=
+begin
+  rw ←@ennreal.le_rpow_one_div_iff _ _ (1/p) (by simp [lt_of_lt_of_le zero_lt_one hp1]),
+  rw one_div_one_div,
+  exact add_rpow_le_rpow_add _ _ hp1,
+end
+
+theorem rpow_add_rpow_le {p q : ℝ} (a b : ennreal) (hp_pos : 0 < p) (hpq : p ≤ q) :
+  (a ^ q + b ^ q) ^ (1/q) ≤ (a ^ p + b ^ p) ^ (1/p) :=
+begin
+  have h_rpow : ∀ a : ennreal, a^q = (a^p)^(q/p),
+    from λ a, by rw [←ennreal.rpow_mul, div_eq_inv_mul, ←mul_assoc,
+      _root_.mul_inv_cancel hp_pos.ne.symm, one_mul],
+  have h_rpow_add_rpow_le_add : ((a^p)^(q/p) + (b^p)^(q/p)) ^ (1/(q/p)) ≤ a^p + b^p,
+  { refine rpow_add_rpow_le_add (a^p) (b^p) _,
+    rwa one_le_div hp_pos, },
+  rw [h_rpow a, h_rpow b, ennreal.le_rpow_one_div_iff hp_pos, ←ennreal.rpow_mul, mul_comm,
+    mul_one_div],
+  rwa one_div_div at h_rpow_add_rpow_le_add,
+end
+
+lemma rpow_add_le_add_rpow {p : ℝ} (a b : ennreal) (hp_pos : 0 < p) (hp1 : p ≤ 1) :
+  (a + b) ^ p ≤ a ^ p + b ^ p :=
+begin
+  have h := rpow_add_rpow_le a b hp_pos hp1,
+  rw one_div_one at h,
+  repeat { rw ennreal.rpow_one at h },
+  exact (ennreal.le_rpow_one_div_iff hp_pos).mp h,
+end
+
 end ennreal
 
 section lintegral

src/analysis/special_functions/pow.lean

@@ -1318,6 +1318,16 @@ begin
   { simp [h], },
 end
 
+lemma div_rpow_of_nonneg (x y : ennreal) {z : ℝ} (hz : 0 ≤ z) :
+  (x / y) ^ z = x ^ z / y ^ z :=
+begin
+  by_cases h0 : z = 0,
+  { simp [h0], },
+  rw ←ne.def at h0,
+  have hz_pos : 0 < z, from lt_of_le_of_ne hz h0.symm,
+  rw [div_eq_mul_inv, mul_rpow_of_nonneg x y⁻¹ hz, inv_rpow_of_pos hz_pos, ←div_eq_mul_inv],
+end
+
 lemma rpow_le_rpow {x y : ennreal} {z : ℝ} (h₁ : x ≤ y) (h₂ : 0 ≤ z) : x^z ≤ y^z :=
 begin
   rcases le_iff_eq_or_lt.1 h₂ with H|H, { simp [← H, le_refl] },
@@ -1408,6 +1418,18 @@ begin
           nnreal.rpow_le_rpow_of_exponent_ge (bot_lt_iff_ne_bot.mpr h) hx1 hyz] }
 end
 
+lemma rpow_le_self_of_le_one {x : ennreal} {z : ℝ} (hx : x ≤ 1) (h_one_le : 1 ≤ z) : x ^ z ≤ x :=
+begin
+  nth_rewrite 1 ←ennreal.rpow_one x,
+  exact ennreal.rpow_le_rpow_of_exponent_ge hx h_one_le,
+end
+
+lemma le_rpow_self_of_one_le {x : ennreal} {z : ℝ} (hx : 1 ≤ x) (h_one_le : 1 ≤ z) : x ≤ x ^ z :=
+begin
+  nth_rewrite 0 ←ennreal.rpow_one x,
+  exact ennreal.rpow_le_rpow_of_exponent_le hx h_one_le,
+end
+
 lemma rpow_pos_of_nonneg {p : ℝ} {x : ennreal} (hx_pos : 0 < x) (hp_nonneg : 0 ≤ p) : 0 < x^p :=
 begin
   by_cases hp_zero : p = 0,

src/measure_theory/integration.lean

@@ -1632,6 +1632,22 @@ lemma lintegral_dirac [measurable_singleton_class α] (a : α) (f : α → ennre
   ∫⁻ a, f a ∂(dirac a) = f a :=
 by simp [lintegral_congr_ae (ae_eq_dirac f)]
 
+lemma lintegral_count' {f : α → ennreal} (hf : measurable f) :
+  ∫⁻ a, f a ∂count = ∑' a, f a :=
+begin
+  rw [count, lintegral_sum_measure],
+  congr,
+  exact funext (λ a, lintegral_dirac' a hf),
+end
+
+lemma lintegral_count [measurable_singleton_class α] (f : α → ennreal) :
+  ∫⁻ a, f a ∂count = ∑' a, f a :=
+begin
+  rw [count, lintegral_sum_measure],
+  congr,
+  exact funext (λ a, lintegral_dirac a f),
+end
+
 lemma ae_lt_top {f : α → ennreal} (hf : measurable f) (h2f : ∫⁻ x, f x ∂μ < ⊤) :
   ∀ᵐ x ∂μ, f x < ⊤ :=
 begin

src/measure_theory/lp_space.lean

@@ -512,22 +512,64 @@ begin
   exact snorm'_add_le hf hg hq1_real,
 end
 
-section second_countable_topology
-variable [topological_space.second_countable_topology E]
+lemma snorm_add_lt_top_of_one_le {f g : α → E} (hf : mem_ℒp f q μ) (hg : mem_ℒp g q μ)
+  (hq1 : 1 ≤ q) :
+  snorm (f + g) q μ < ⊤ :=
+lt_of_le_of_lt (snorm_add_le hf.1 hg.1 hq1) (ennreal.add_lt_top.mpr ⟨hf.2, hg.2⟩)
+
+lemma snorm'_add_lt_top_of_le_one {f g : α → E} (hf : ae_measurable f μ) (hg : ae_measurable g μ)
+  (hf_snorm : snorm' f p μ < ⊤) (hg_snorm : snorm' g p μ < ⊤) (hp_pos : 0 < p) (hp1 : p ≤ 1) :
+  snorm' (f + g) p μ < ⊤ :=
+calc (∫⁻ a, ↑(nnnorm ((f + g) a)) ^ p ∂μ) ^ (1 / p)
+    ≤ (∫⁻ a, (((λ a, (nnnorm (f a) : ennreal))
+        + (λ a, (nnnorm (g a) : ennreal))) a) ^ p ∂μ) ^ (1 / p) :
+begin
+  refine @ennreal.rpow_le_rpow _ _ (1/p) _ (by simp [hp_pos.le]),
+  refine lintegral_mono (λ a, ennreal.rpow_le_rpow _ hp_pos.le),
+  simp [←ennreal.coe_add, nnnorm_add_le],
+end
+... ≤ (∫⁻ a, (nnnorm (f a) : ennreal) ^ p + (nnnorm (g a) : ennreal) ^ p ∂μ) ^ (1 / p) :
+begin
+  refine @ennreal.rpow_le_rpow _ _ (1/p) (lintegral_mono (λ a, _)) (by simp [hp_pos.le]),
+  exact ennreal.rpow_add_le_add_rpow _ _ hp_pos hp1,
+end
+... < ⊤ :
+begin
+  refine @ennreal.rpow_lt_top_of_nonneg _ (1/p) (by simp [hp_pos.le]) _,
+  rw [lintegral_add' hf.nnnorm.ennreal_coe.ennreal_rpow_const
+    hg.nnnorm.ennreal_coe.ennreal_rpow_const, ennreal.add_ne_top, ←lt_top_iff_ne_top,
+    ←lt_top_iff_ne_top],
+  exact ⟨lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top hp_pos hf_snorm,
+    lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top hp_pos hg_snorm⟩,
+end
 
-/-- TODO: prove mem_ℒp.add for all `q:ennreal`. `snorm_add_le` cannot be used for `q < 1` but the
-result still holds. -/
-lemma mem_ℒp.add {f g : α → E} (hf : mem_ℒp f q μ) (hg : mem_ℒp g q μ) (hq1 : 1 ≤ q) :
-  mem_ℒp (f + g) q μ :=
+lemma snorm_add_lt_top {f g : α → E} (hf : mem_ℒp f q μ) (hg : mem_ℒp g q μ) :
+  snorm (f + g) q μ < ⊤ :=
 begin
-  refine ⟨ae_measurable.add hf.1 hg.1, lt_of_le_of_lt (snorm_add_le hf.1 hg.1 hq1) _⟩,
-  rw ennreal.add_lt_top,
-  exact ⟨hf.2, hg.2⟩,
+  by_cases h0 : q = 0,
+  { simp [h0], },
+  rw ←ne.def at h0,
+  cases le_total 1 q with hq1 hq1,
+  { exact snorm_add_lt_top_of_one_le hf hg hq1, },
+  have hq_top : q ≠ ⊤, from (lt_of_le_of_lt hq1 ennreal.coe_lt_top).ne,
+  have hq_pos : 0 < q.to_real,
+  { rw [←ennreal.zero_to_real, @ennreal.to_real_lt_to_real 0 q ennreal.coe_ne_top hq_top],
+    exact ((zero_le q).lt_of_ne h0.symm), },
+  have hq1_real : q.to_real ≤ 1,
+  { rwa [←ennreal.one_to_real, @ennreal.to_real_le_to_real q 1 hq_top ennreal.coe_ne_top], },
+  rw snorm_eq_snorm' h0 hq_top,
+  rw [mem_ℒp, snorm_eq_snorm' h0 hq_top] at hf hg,
+  exact snorm'_add_lt_top_of_le_one hf.1 hg.1 hf.2 hg.2 hq_pos hq1_real,
 end
 
-lemma mem_ℒp.sub {f g : α → E} (hf : mem_ℒp f q μ) (hg : mem_ℒp g q μ) (hq1 : 1 ≤ q) :
-  mem_ℒp (f-g) q μ :=
-by { rw sub_eq_add_neg, exact hf.add hg.neg hq1 }
+section second_countable_topology
+variable [topological_space.second_countable_topology E]
+
+lemma mem_ℒp.add {f g : α → E} (hf : mem_ℒp f q μ) (hg : mem_ℒp g q μ) : mem_ℒp (f + g) q μ :=
+⟨ae_measurable.add hf.1 hg.1, snorm_add_lt_top hf hg⟩
+
+lemma mem_ℒp.sub {f g : α → E} (hf : mem_ℒp f q μ) (hg : mem_ℒp g q μ) : mem_ℒp (f - g) q μ :=
+by { rw sub_eq_add_neg, exact hf.add hg.neg }
 
 end second_countable_topology