feat(analysis/mean_inequalities): add young_inequality for nnreal and ennreal with real exponents (#5242)

The existing young_inequality for nnreal has nnreal exponents. This adds a version with real exponents with the is_conjugate_exponent property, and a similar version for ennreal with real exponents.



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

Author: RemyDegenne

src/analysis/mean_inequalities.lean

@@ -292,6 +292,15 @@ theorem young_inequality (a b : ℝ≥0) {p q : ℝ≥0} (hp : 1 < p) (hpq : 1 /
   a * b ≤ a^(p:ℝ) / p + b^(q:ℝ) / q :=
 real.young_inequality_of_nonneg a.coe_nonneg b.coe_nonneg ⟨hp, nnreal.coe_eq.2 hpq⟩
 
+/-- Young's inequality, `ℝ≥0` version with real conjugate exponents. -/
+theorem young_inequality_real (a b : ℝ≥0) {p q : ℝ} (hpq : p.is_conjugate_exponent q) :
+  a * b ≤ a ^ p / nnreal.of_real p + b ^ q / nnreal.of_real q :=
+begin
+  nth_rewrite 0 ←coe_of_real p hpq.nonneg,
+  nth_rewrite 0 ←coe_of_real q hpq.symm.nonneg,
+  exact young_inequality a b hpq.one_lt_nnreal hpq.inv_add_inv_conj_nnreal,
+end
+
 /-- Hölder inequality: the scalar product of two functions is bounded by the product of their
 `L^p` and `L^q` norms when `p` and `q` are conjugate exponents. Version for sums over finite sets,
 with `ℝ≥0`-valued functions. -/
@@ -444,6 +453,22 @@ end real
 
 namespace ennreal
 
+/-- Young's inequality, `ennreal` version with real conjugate exponents. -/
+theorem young_inequality (a b : ennreal) {p q : ℝ} (hpq : p.is_conjugate_exponent q) :
+  a * b ≤ a ^ p / ennreal.of_real p + b ^ q / ennreal.of_real q :=
+begin
+  by_cases h : a = ⊤ ∨ b = ⊤,
+  { refine le_trans le_top (le_of_eq _),
+    repeat {rw ennreal.div_def},
+    cases h; rw h; simp [h, hpq.pos, hpq.symm.pos], },
+  push_neg at h, -- if a ≠ ⊤ and b ≠ ⊤, use the nnreal version: nnreal.young_inequality_real
+  rw [←coe_to_nnreal h.left, ←coe_to_nnreal h.right, ←coe_mul,
+    coe_rpow_of_nonneg _ hpq.nonneg, coe_rpow_of_nonneg _ hpq.symm.nonneg, ennreal.of_real,
+    ennreal.of_real, ←@coe_div (nnreal.of_real p) _ (by simp [hpq.pos]),
+    ←@coe_div (nnreal.of_real q) _ (by simp [hpq.symm.pos]), ←coe_add, coe_le_coe],
+  exact nnreal.young_inequality_real a.to_nnreal b.to_nnreal hpq,
+end
+
 variables (f g : ι → ennreal)  {p q : ℝ}
 
 /-- Hölder inequality: the scalar product of two functions is bounded by the product of their

src/data/real/conjugate_exponents.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Yury Kudryashov
 -/
-import data.real.basic
+import data.real.nnreal
 
 /-!
 # Real conjugate exponents
@@ -81,6 +81,16 @@ by simpa only [sub_mul, sub_eq_iff_eq_add, one_mul] using h.sub_one_mul_conj
 { one_lt := by { rw [h.conj_eq], exact (one_lt_div h.sub_one_pos).mpr (sub_one_lt p) },
   inv_add_inv_conj := by simpa [add_comm] using h.inv_add_inv_conj }
 
+lemma one_lt_nnreal : 1 < nnreal.of_real p :=
+begin
+  rw [←nnreal.of_real_one, nnreal.of_real_lt_of_real_iff h.pos],
+  exact h.one_lt,
+end
+
+lemma inv_add_inv_conj_nnreal : 1 / nnreal.of_real p + 1 / nnreal.of_real q = 1 :=
+by rw [←nnreal.of_real_one, ←nnreal.of_real_div' h.nonneg, ←nnreal.of_real_div' h.symm.nonneg,
+  ←nnreal.of_real_add h.one_div_nonneg h.symm.one_div_nonneg, h.inv_add_inv_conj]
+
 end is_conjugate_exponent
 
 lemma is_conjugate_exponent_iff {p q : ℝ} (h : 1 < p) :

src/data/real/nnreal.lean

@@ -658,6 +658,25 @@ by simpa using @div_eq_div_iff a b c 1 hb one_ne_zero
 @[field_simps] lemma eq_div_iff {a b c : ℝ≥0} (hb : b ≠ 0) : c = a / b ↔ c * b = a :=
 by simpa using @div_eq_div_iff c 1 a b one_ne_zero hb
 
+lemma of_real_inv {x : ℝ} :
+  nnreal.of_real x⁻¹ = (nnreal.of_real x)⁻¹ :=
+begin
+  by_cases hx : 0 ≤ x,
+  { nth_rewrite 0 ← coe_of_real x hx,
+    rw [←nnreal.coe_inv, of_real_coe], },
+  { have hx' := le_of_not_ge hx,
+    rw [of_real_eq_zero.mpr hx', inv_zero, of_real_eq_zero.mpr (inv_nonpos.mpr hx')], },
+end
+
+lemma of_real_div {x y : ℝ} (hx : 0 ≤ x) :
+  nnreal.of_real (x / y) = nnreal.of_real x / nnreal.of_real y :=
+by rw [div_def, ←of_real_inv, ←of_real_mul hx, div_eq_mul_inv]
+
+lemma of_real_div' {x y : ℝ} (hy : 0 ≤ y) :
+  nnreal.of_real (x / y) = nnreal.of_real x / nnreal.of_real y :=
+by rw [div_def, ←of_real_inv, mul_comm, ←@of_real_mul y⁻¹ _ (by simp [hy]), mul_comm,
+  div_eq_mul_inv]
+
 end inv
 
 section pow