feat(measure_theory/lp_space): add lemmas about the monotonicity of t…

…he Lp seminorm (#5395)

Also add a lemma mem_Lp.const_smul for a normed space.



Co-authored-by: Rémy Degenne <remydegenne@gmail.com>

src/analysis/mean_inequalities.lean

@@ -802,6 +802,47 @@ begin
   end
 end
 
+lemma lintegral_Lp_mul_le_Lq_mul_Lr {α} [measurable_space α] {p q r : ℝ} (hp0_lt : 0 < p)
+  (hpq : p < q) (hpqr : 1/p = 1/q + 1/r) (μ : measure α) {f g : α → ennreal}
+  (hf : measurable f) (hg : measurable g) :
+  (∫⁻ a, ((f * g) a)^p ∂μ) ^ (1/p) ≤ (∫⁻ a, (f a)^q ∂μ) ^ (1/q) * (∫⁻ a, (g a)^r ∂μ) ^ (1/r) :=
+begin
+  have hp0_ne : p ≠ 0, from (ne_of_lt hp0_lt).symm,
+  have hp0 : 0 ≤ p, from le_of_lt hp0_lt,
+  have hq0_lt : 0 < q, from lt_of_le_of_lt hp0 hpq,
+  have hq0_ne : q ≠ 0, from (ne_of_lt hq0_lt).symm,
+  have h_one_div_r : 1/r = 1/p - 1/q, by simp [hpqr],
+  have hr0_ne : r ≠ 0,
+  { have hr_inv_pos : 0 < 1/r,
+    by rwa [h_one_div_r, sub_pos, one_div_lt_one_div hq0_lt hp0_lt],
+    rw [one_div, _root_.inv_pos] at hr_inv_pos,
+    exact (ne_of_lt hr_inv_pos).symm, },
+  let p2 := q/p,
+  let q2 := p2.conjugate_exponent,
+  have hp2q2 : p2.is_conjugate_exponent q2,
+  from real.is_conjugate_exponent_conjugate_exponent (by simp [lt_div_iff, hpq, hp0_lt]),
+  calc (∫⁻ (a : α), ((f * g) a) ^ p ∂μ) ^ (1 / p)
+      = (∫⁻ (a : α), (f a)^p * (g a)^p ∂μ) ^ (1 / p) :
+  by simp_rw [pi.mul_apply, ennreal.mul_rpow_of_nonneg _ _ hp0]
+  ... ≤ ((∫⁻ a, (f a)^(p * p2) ∂ μ)^(1/p2) * (∫⁻ a, (g a)^(p * q2) ∂ μ)^(1/q2)) ^ (1/p) :
+  begin
+    refine ennreal.rpow_le_rpow _ (by simp [hp0]),
+    simp_rw ennreal.rpow_mul,
+    exact ennreal.lintegral_mul_le_Lp_mul_Lq μ hp2q2 hf.ennreal_rpow_const hg.ennreal_rpow_const,
+  end
+  ... = (∫⁻ (a : α), (f a) ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), (g a) ^ r ∂μ) ^ (1 / r) :
+  begin
+    rw [@ennreal.mul_rpow_of_nonneg _ _ (1/p) (by simp [hp0]), ←ennreal.rpow_mul,
+      ←ennreal.rpow_mul],
+    have hpp2 : p * p2 = q,
+    { symmetry, rw [mul_comm, ←div_eq_iff hp0_ne], },
+    have hpq2 : p * q2 = r,
+    { rw [← inv_inv' r, ← one_div, ← one_div, h_one_div_r],
+      field_simp [q2, real.conjugate_exponent, p2, hp0_ne, hq0_ne] },
+    simp_rw [div_mul_div, mul_one, mul_comm p2, mul_comm q2, hpp2, hpq2],
+  end
+end
+
 lemma lintegral_mul_rpow_le_lintegral_rpow_mul_lintegral_rpow {p q : ℝ}
   (hpq : p.is_conjugate_exponent q) {f g : α → ennreal} (hf : measurable f) (hg : measurable g)
   (hf_top : ∫⁻ a, (f a) ^ p ∂μ ≠ ⊤) :

src/measure_theory/lp_space.lean

@@ -104,7 +104,77 @@ variable [borel_space E]
 lemma mem_ℒp.neg {f : α → E} (hf : mem_ℒp f p μ) : mem_ℒp (-f) p μ :=
 ⟨measurable.neg hf.1, by simp [hf.right]⟩
 
+lemma snorm_le_snorm_mul_rpow_measure_univ {p q : ℝ} (hp0_lt : 0 < p) (hpq : p ≤ q) (μ : measure α)
+  {f : α → E} (hf : measurable f) :
+  snorm f p μ ≤ snorm f q μ * (μ set.univ) ^ (1/p - 1/q) :=
+begin
+  have hq0_lt : 0 < q, from lt_of_lt_of_le hp0_lt hpq,
+  by_cases hpq_eq : p = q,
+  { rw [hpq_eq, sub_self, ennreal.rpow_zero, mul_one],
+    exact le_refl _, },
+  have hpq : p < q, from lt_of_le_of_ne hpq hpq_eq,
+  let g := λ a : α, (1 : ennreal),
+  have h_rw : ∫⁻ a, ↑(nnnorm (f a))^p ∂ μ = ∫⁻ a, (nnnorm (f a) * (g a))^p ∂ μ,
+  from lintegral_congr (λ a, by simp),
+  repeat {rw snorm},
+  rw h_rw,
+  let r := p * q / (q - p),
+  have hpqr : 1/p = 1/q + 1/r,
+  { field_simp [(ne_of_lt hp0_lt).symm,
+      (ne_of_lt hq0_lt).symm],
+    ring, },
+  calc (∫⁻ (a : α), (↑(nnnorm (f a)) * g a) ^ p ∂μ) ^ (1/p)
+      ≤ (∫⁻ (a : α), ↑(nnnorm (f a)) ^ q ∂μ) ^ (1/q) * (∫⁻ (a : α), (g a) ^ r ∂μ) ^ (1/r) :
+    ennreal.lintegral_Lp_mul_le_Lq_mul_Lr hp0_lt hpq hpqr μ hf.nnnorm.ennreal_coe measurable_const
+  ... = (∫⁻ (a : α), ↑(nnnorm (f a)) ^ q ∂μ) ^ (1/q) * μ set.univ ^ (1/p - 1/q) :
+    by simp [hpqr],
+end
+
+lemma snorm_le_snorm_of_exponent_le {p q : ℝ} (hp0_lt : 0 < p) (hpq : p ≤ q) (μ : measure α)
+  [probability_measure μ] {f : α → E} (hf : measurable f) :
+  snorm f p μ ≤ snorm f q μ :=
+begin
+  have h_le_μ := snorm_le_snorm_mul_rpow_measure_univ hp0_lt hpq μ hf,
+  rwa [measure_univ, ennreal.one_rpow, mul_one] at h_le_μ,
+end
+
+lemma mem_ℒp.mem_ℒp_of_exponent_le {p q : ℝ} {μ : measure α} [finite_measure μ] {f : α → E}
+  (hfq : mem_ℒp f q μ) (hp_pos : 0 < p) (hpq : p ≤ q) :
+  mem_ℒp f p μ :=
+begin
+  cases hfq with hfq_m hfq_lt_top,
+  split,
+  { exact hfq_m, },
+  have hq_pos : 0 < q, from lt_of_lt_of_le  hp_pos hpq,
+  suffices h_snorm : snorm f p μ < ⊤,
+  { have h_top_eq : (⊤ : ennreal) = ⊤ ^ (1/p), by simp [hp_pos],
+    rw [snorm, h_top_eq] at h_snorm,
+    have h_snorm_pow : ((∫⁻ (a : α), ↑(nnnorm (f a)) ^ p ∂μ) ^ (1/p)) ^ p < (⊤ ^ (1/p)) ^ p,
+    from ennreal.rpow_lt_rpow h_snorm hp_pos,
+    rw [←ennreal.rpow_mul, ←ennreal.rpow_mul] at h_snorm_pow,
+    simpa [(ne_of_lt hp_pos).symm] using h_snorm_pow, },
+  calc snorm f p μ
+      ≤ snorm f q μ * (μ set.univ) ^ (1/p - 1/q) :
+    snorm_le_snorm_mul_rpow_measure_univ hp_pos hpq μ hfq_m
+  ... < ⊤ :
+  begin
+    rw ennreal.mul_lt_top_iff,
+    left,
+    split,
+    { exact mem_ℒp.snorm_lt_top (le_of_lt hq_pos) ⟨hfq_m, hfq_lt_top⟩, },
+    { refine ennreal.rpow_lt_top_of_nonneg _ (measure_ne_top μ set.univ),
+      rwa [le_sub, sub_zero, one_div, one_div, inv_le_inv hq_pos hp_pos], },
+  end
+end
+
+lemma mem_ℒp.integrable (hp1 : 1 ≤ p) {f : α → E} [finite_measure μ] (hfp : mem_ℒp f p μ) :
+  integrable f μ :=
+begin
+  rw ←mem_ℒp_one_iff_integrable,
+  exact hfp.mem_ℒp_of_exponent_le zero_lt_one hp1,
+end
 
+section second_countable_topology
 variable [topological_space.second_countable_topology E]
 
 lemma mem_ℒp.add {f g : α → E} (hf : mem_ℒp f p μ) (hg : mem_ℒp g p μ) (hp1 : 1 ≤ p) :
@@ -128,6 +198,35 @@ begin
     hg.1.nnnorm.ennreal_coe hg.2 hp1,
 end
 
+end second_countable_topology
+
+section normed_space
+
+variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 E]
+
+lemma mem_ℒp.const_smul {f : α → E} (hfp : mem_ℒp f p μ) (c : 𝕜) (hp0 : 0 ≤ p) :
+  mem_ℒp (c • f) p μ :=
+begin
+  split,
+  { exact measurable.const_smul hfp.1 c, },
+  simp_rw [pi.smul_apply, nnnorm_smul, ennreal.coe_mul, ennreal.mul_rpow_of_nonneg _ _ hp0],
+  rw lintegral_const_mul _ hfp.1.nnnorm.ennreal_coe.ennreal_rpow_const,
+  exact ennreal.mul_lt_top (ennreal.rpow_lt_top_of_nonneg hp0 ennreal.coe_ne_top) hfp.2,
+end
+
+lemma snorm_smul_le_mul_snorm [measurable_space 𝕜] [opens_measurable_space 𝕜] {q r : ℝ}
+  {f : α → E} (hf : measurable f) {φ : α → 𝕜} (hφ : measurable φ)
+  (hp0_lt : 0 < p) (hpq : p < q) (hpqr : 1/p = 1/q + 1/r) :
+  snorm (φ • f) p μ ≤ snorm φ q μ * snorm f r μ :=
+begin
+  rw snorm,
+  simp_rw [pi.smul_apply', nnnorm_smul, ennreal.coe_mul],
+  exact ennreal.lintegral_Lp_mul_le_Lq_mul_Lr hp0_lt hpq hpqr μ hφ.nnnorm.ennreal_coe
+    hf.nnnorm.ennreal_coe,
+end
+
+end normed_space
+
 end borel_space
 
 end ℒp_space