feat(measure_theory/integral/bochner): Hölder's inequality for real n…

…onnegative functions (#16291)

We already have several versions of Hölder's inequality for the Lebesgue integral and functions with values in nnreal or ennreal. This PR introduces two versions of this inequality for the Bochner integral, one of which applies to nonnegative real functions.

src/measure_theory/function/ess_sup.lean

@@ -252,6 +252,9 @@ limsup_eq_zero_iff
 lemma ess_sup_const_mul {a : ℝ≥0∞} : ess_sup (λ (x : α), a * (f x)) μ = a * ess_sup f μ :=
 limsup_const_mul
 
+lemma ess_sup_mul_le (f g : α → ℝ≥0∞) : ess_sup (f * g) μ ≤ ess_sup f μ * ess_sup g μ :=
+limsup_mul_le f g
+
 lemma ess_sup_add_le (f g : α → ℝ≥0∞) : ess_sup (f + g) μ ≤ ess_sup f μ + ess_sup g μ :=
 limsup_add_le f g
 

src/measure_theory/function/lp_space.lean

@@ -1217,6 +1217,113 @@ begin
     hf.ennnorm,
 end
 
+lemma snorm_smul_le_snorm_top_mul_snorm (p : ℝ≥0∞)
+  {f : α → E} (hf : ae_strongly_measurable f μ) (φ : α → 𝕜) :
+  snorm (φ • f) p μ ≤ snorm φ ∞ μ * snorm f p μ :=
+begin
+  by_cases hp_top : p = ∞,
+  { simp_rw [hp_top, snorm_exponent_top, snorm_ess_sup, pi.smul_apply', nnnorm_smul,
+      ennreal.coe_mul],
+    exact ennreal.ess_sup_mul_le _ _, },
+  by_cases hp_zero : p = 0,
+  { simp only [hp_zero, snorm_exponent_zero, mul_zero, le_zero_iff], },
+  simp_rw [snorm_eq_lintegral_rpow_nnnorm hp_zero hp_top, snorm_exponent_top, snorm_ess_sup],
+  calc (∫⁻ x, ↑∥(φ • f) x∥₊ ^ p.to_real ∂μ) ^ (1 / p.to_real)
+      = (∫⁻ x, ↑∥φ x∥₊ ^ p.to_real * ↑∥f x∥₊ ^ p.to_real ∂μ) ^ (1 / p.to_real) :
+    begin
+      congr,
+      ext1 x,
+      rw [pi.smul_apply', nnnorm_smul, ennreal.coe_mul,
+        ennreal.mul_rpow_of_nonneg _ _ (ennreal.to_real_nonneg)],
+    end
+  ... ≤ (∫⁻ x, (ess_sup (λ x, ↑∥φ x∥₊) μ) ^ p.to_real * ↑∥f x∥₊ ^ p.to_real ∂μ) ^ (1 / p.to_real) :
+    begin
+      refine ennreal.rpow_le_rpow _ _,
+      swap, { rw one_div_nonneg, exact ennreal.to_real_nonneg, },
+      refine lintegral_mono_ae _,
+      filter_upwards [@ennreal.ae_le_ess_sup _ _ μ (λ x, ↑∥φ x∥₊)] with x hx,
+      refine ennreal.mul_le_mul _ le_rfl,
+      exact ennreal.rpow_le_rpow hx ennreal.to_real_nonneg,
+    end
+  ... = ess_sup (λ x, ↑∥φ x∥₊) μ * (∫⁻ x, ↑∥f x∥₊ ^ p.to_real ∂μ) ^ (1 / p.to_real) :
+    begin
+      rw lintegral_const_mul'',
+      swap, { exact hf.nnnorm.ae_measurable.coe_nnreal_ennreal.pow ae_measurable_const, },
+      rw ennreal.mul_rpow_of_nonneg,
+      swap, { rw one_div_nonneg, exact ennreal.to_real_nonneg, },
+      rw [← ennreal.rpow_mul, one_div, mul_inv_cancel, ennreal.rpow_one],
+      rw [ne.def, ennreal.to_real_eq_zero_iff, auto.not_or_eq],
+      exact ⟨hp_zero, hp_top⟩,
+    end
+end
+
+lemma snorm_smul_le_snorm_mul_snorm_top (p : ℝ≥0∞)
+  (f : α → E) {φ : α → 𝕜} (hφ : ae_strongly_measurable φ μ) :
+  snorm (φ • f) p μ ≤ snorm φ p μ * snorm f ∞ μ :=
+begin
+  rw ← snorm_norm,
+  simp_rw [pi.smul_apply', norm_smul],
+  have : (λ x, ∥φ x∥ * ∥f x∥) = (λ x, ∥f x∥) • (λ x, ∥φ x∥),
+  { rw [smul_eq_mul, mul_comm], refl, },
+  rw this,
+  have h := snorm_smul_le_snorm_top_mul_snorm p hφ.norm (λ x, ∥f x∥),
+  refine h.trans_eq _,
+  simp_rw snorm_norm,
+  rw mul_comm,
+end
+
+/-- Hölder's inequality, as an inequality on the `ℒp` seminorm of a scalar product `φ • f`. -/
+lemma snorm_smul_le_mul_snorm {p q r : ℝ≥0∞}
+  {f : α → E} (hf : ae_strongly_measurable f μ) {φ : α → 𝕜} (hφ : ae_strongly_measurable φ μ)
+  (hpqr : 1/p = 1/q + 1/r) :
+  snorm (φ • f) p μ ≤ snorm φ q μ * snorm f r μ :=
+begin
+  by_cases hp_zero : p = 0,
+  { simp [hp_zero], },
+  have hq_ne_zero : q ≠ 0,
+  { intro hq_zero,
+    simp only [hq_zero, hp_zero, one_div, ennreal.inv_zero, ennreal.top_add,
+      ennreal.inv_eq_top] at hpqr,
+    exact hpqr, },
+  have hr_ne_zero : r ≠ 0,
+  { intro hr_zero,
+    simp only [hr_zero, hp_zero, one_div, ennreal.inv_zero, ennreal.add_top,
+      ennreal.inv_eq_top] at hpqr,
+    exact hpqr, },
+  by_cases hq_top : q = ∞,
+  { have hpr : p = r,
+    { simpa only [hq_top, one_div, ennreal.div_top, zero_add, inv_inj] using hpqr, },
+    rw [← hpr, hq_top],
+    exact snorm_smul_le_snorm_top_mul_snorm p hf φ, },
+  by_cases hr_top : r = ∞,
+  { have hpq : p = q,
+    { simpa only [hr_top, one_div, ennreal.div_top, add_zero, inv_inj] using hpqr, },
+    rw [← hpq, hr_top],
+    exact snorm_smul_le_snorm_mul_snorm_top p f hφ, },
+  have hpq : p < q,
+  { suffices : 1 / q < 1 / p,
+    { rwa [one_div, one_div, ennreal.inv_lt_inv] at this, },
+    rw hpqr,
+    refine ennreal.lt_add_right _ _,
+    { simp only [hq_ne_zero, one_div, ne.def, ennreal.inv_eq_top, not_false_iff], },
+    { simp only [hr_top, one_div, ne.def, ennreal.inv_eq_zero, not_false_iff], }, },
+  rw [snorm_eq_snorm' hp_zero (hpq.trans_le le_top).ne, snorm_eq_snorm' hq_ne_zero hq_top,
+    snorm_eq_snorm' hr_ne_zero hr_top],
+  refine snorm'_smul_le_mul_snorm' hf hφ _ _ _,
+  { exact ennreal.to_real_pos hp_zero (hpq.trans_le le_top).ne, },
+  { exact ennreal.to_real_strict_mono hq_top hpq, },
+  rw [← ennreal.one_to_real, ← ennreal.to_real_div, ← ennreal.to_real_div, ← ennreal.to_real_div,
+    hpqr, ennreal.to_real_add],
+  { simp only [hq_ne_zero, one_div, ne.def, ennreal.inv_eq_top, not_false_iff], },
+  { simp only [hr_ne_zero, one_div, ne.def, ennreal.inv_eq_top, not_false_iff], },
+end
+
+lemma mem_ℒp.smul {p q r : ℝ≥0∞} {f : α → E} {φ : α → 𝕜}
+  (hf : mem_ℒp f r μ) (hφ : mem_ℒp φ q μ) (hpqr : 1/p = 1/q + 1/r) :
+  mem_ℒp (φ • f) p μ :=
+⟨hφ.1.smul hf.1, (snorm_smul_le_mul_snorm hf.1 hφ.1 hpqr).trans_lt
+  (ennreal.mul_lt_top hφ.snorm_ne_top hf.snorm_ne_top)⟩
+
 end normed_space
 
 section monotonicity

src/measure_theory/integral/bochner.lean

@@ -1422,6 +1422,80 @@ begin
     rw abs_of_nonneg (hf_nonneg x), },
 end
 
+/-- Hölder's inequality for the integral of a product of norms. The integral of the product of two
+norms of functions is bounded by the product of their `ℒp` and `ℒq` seminorms when `p` and `q` are
+conjugate exponents. -/
+theorem integral_mul_norm_le_Lp_mul_Lq {E} [normed_add_comm_group E] {f g : α → E}
+  {p q : ℝ} (hpq : p.is_conjugate_exponent q)
+  (hf : mem_ℒp f (ennreal.of_real p) μ) (hg : mem_ℒp g (ennreal.of_real q) μ) :
+  ∫ a, ∥f a∥ * ∥g a∥ ∂μ ≤ (∫ a, ∥f a∥ ^ p ∂μ) ^ (1/p) * (∫ a, ∥g a∥ ^ q ∂μ) ^ (1/q) :=
+begin
+  -- translate the Bochner integrals into Lebesgue integrals.
+  rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae,
+    integral_eq_lintegral_of_nonneg_ae],
+  rotate 1,
+  { exact eventually_of_forall (λ x, real.rpow_nonneg_of_nonneg (norm_nonneg _) _), },
+  { exact (hg.1.norm.ae_measurable.pow ae_measurable_const).ae_strongly_measurable, },
+  { exact eventually_of_forall (λ x, real.rpow_nonneg_of_nonneg (norm_nonneg _) _),},
+  { exact (hf.1.norm.ae_measurable.pow ae_measurable_const).ae_strongly_measurable, },
+  { exact eventually_of_forall (λ x, mul_nonneg (norm_nonneg _) (norm_nonneg _)), },
+  { exact hf.1.norm.mul hg.1.norm, },
+  rw [ennreal.to_real_rpow, ennreal.to_real_rpow, ← ennreal.to_real_mul],
+  -- replace norms by nnnorm
+  have h_left : ∫⁻ a, ennreal.of_real (∥f a∥ * ∥g a∥) ∂μ
+    = ∫⁻ a, ((λ x, (∥f x∥₊ : ℝ≥0∞)) * (λ x, ∥g x∥₊)) a ∂μ,
+  { simp_rw [pi.mul_apply, ← of_real_norm_eq_coe_nnnorm, ennreal.of_real_mul (norm_nonneg _)], },
+  have h_right_f : ∫⁻ a, ennreal.of_real (∥f a∥ ^ p) ∂μ = ∫⁻ a, ∥f a∥₊ ^ p ∂μ,
+  { refine lintegral_congr (λ x, _),
+    rw [← of_real_norm_eq_coe_nnnorm, ennreal.of_real_rpow_of_nonneg (norm_nonneg _) hpq.nonneg], },
+  have h_right_g : ∫⁻ a, ennreal.of_real (∥g a∥ ^ q) ∂μ = ∫⁻ a, ∥g a∥₊ ^ q ∂μ,
+  { refine lintegral_congr (λ x, _),
+    rw [← of_real_norm_eq_coe_nnnorm,
+      ennreal.of_real_rpow_of_nonneg (norm_nonneg _) hpq.symm.nonneg], },
+  rw [h_left, h_right_f, h_right_g],
+  -- we can now apply `ennreal.lintegral_mul_le_Lp_mul_Lq` (up to the `to_real` application)
+  refine ennreal.to_real_mono _ _,
+  { refine ennreal.mul_ne_top _ _,
+    { convert hf.snorm_ne_top,
+      rw snorm_eq_lintegral_rpow_nnnorm,
+      { rw ennreal.to_real_of_real hpq.nonneg, },
+      { rw [ne.def, ennreal.of_real_eq_zero, not_le],
+        exact hpq.pos, },
+      { exact ennreal.coe_ne_top, }, },
+    { convert hg.snorm_ne_top,
+      rw snorm_eq_lintegral_rpow_nnnorm,
+      { rw ennreal.to_real_of_real hpq.symm.nonneg, },
+      { rw [ne.def, ennreal.of_real_eq_zero, not_le],
+        exact hpq.symm.pos, },
+      { exact ennreal.coe_ne_top, }, }, },
+  { exact ennreal.lintegral_mul_le_Lp_mul_Lq μ hpq hf.1.nnnorm.ae_measurable.coe_nnreal_ennreal
+      hg.1.nnnorm.ae_measurable.coe_nnreal_ennreal, },
+end
+
+/-- Hölder's inequality for functions `α → ℝ`. The integral of the product of two nonnegative
+functions is bounded by the product of their `ℒp` and `ℒq` seminorms when `p` and `q` are conjugate
+exponents. -/
+theorem integral_mul_le_Lp_mul_Lq_of_nonneg {p q : ℝ}
+  (hpq : p.is_conjugate_exponent q) {f g : α → ℝ} (hf_nonneg : 0 ≤ᵐ[μ] f) (hg_nonneg : 0 ≤ᵐ[μ] g)
+  (hf : mem_ℒp f (ennreal.of_real p) μ) (hg : mem_ℒp g (ennreal.of_real q) μ) :
+  ∫ a, f a * g a ∂μ ≤ (∫ a, (f a) ^ p ∂μ) ^ (1/p) * (∫ a, (g a) ^ q ∂μ) ^ (1/q) :=
+begin
+  have h_left : ∫ a, f a * g a ∂μ = ∫ a, ∥f a∥ * ∥g a∥ ∂μ,
+  { refine integral_congr_ae _,
+    filter_upwards [hf_nonneg, hg_nonneg] with x hxf hxg,
+    rw [real.norm_of_nonneg hxf, real.norm_of_nonneg hxg], },
+  have h_right_f : ∫ a, (f a) ^ p ∂μ = ∫ a, ∥f a∥ ^ p ∂μ,
+  { refine integral_congr_ae _,
+    filter_upwards [hf_nonneg] with x hxf,
+    rw real.norm_of_nonneg hxf, },
+  have h_right_g : ∫ a, (g a) ^ q ∂μ = ∫ a, ∥g a∥ ^ q ∂μ,
+  { refine integral_congr_ae _,
+    filter_upwards [hg_nonneg] with x hxg,
+    rw real.norm_of_nonneg hxg, },
+  rw [h_left, h_right_f, h_right_g],
+  exact integral_mul_norm_le_Lp_mul_Lq hpq hf hg,
+end
+
 end properties
 
 mk_simp_attribute integral_simps "Simp set for integral rules."

src/order/filter/ennreal.lean

@@ -95,6 +95,17 @@ begin
     simp only [h_top_le, hfu, if_false], },
 end
 
+lemma limsup_mul_le [countable_Inter_filter f] (u v : α → ℝ≥0∞) :
+  f.limsup (u * v) ≤ f.limsup u * f.limsup v :=
+calc f.limsup (u * v) ≤ f.limsup (λ x, (f.limsup u) * v x) :
+  begin
+    refine limsup_le_limsup _ _,
+    { filter_upwards [@eventually_le_limsup _ f _ u] with x hx,
+      exact ennreal.mul_le_mul hx le_rfl, },
+    { is_bounded_default, },
+  end
+... = f.limsup u * f.limsup v : limsup_const_mul
+
 lemma limsup_add_le [countable_Inter_filter f] (u v : α → ℝ≥0∞) :
   f.limsup (u + v) ≤ f.limsup u + f.limsup v :=
 Inf_le ((eventually_le_limsup u).mp ((eventually_le_limsup v).mono