feat: ENNReal-valued conjugate exponents (#17353)

Define `ENNReal.IsConjExponent`, the `ENNReal` analogue of `Real.IsConjExponent` and `NNReal.IsConjExponent`. This will allow stating Hölder's inequality for the L1 and Linfty norms too.

From LeanAPAP

Mathlib/Data/ENNReal/Operations.lean

@@ -256,6 +256,7 @@ section Cancel
 -- Porting note (#11215): TODO: generalize to `WithTop`
 /-- An element `a` is `AddLECancellable` if `a + b ≤ a + c` implies `b ≤ c` for all `b` and `c`.
   This is true in `ℝ≥0∞` for all elements except `∞`. -/
+@[simp]
 theorem addLECancellable_iff_ne {a : ℝ≥0∞} : AddLECancellable a ↔ a ≠ ∞ := by
   constructor
   · rintro h rfl
@@ -294,11 +295,13 @@ theorem sub_eq_sInf {a b : ℝ≥0∞} : a - b = sInf { d | a ≤ d + b } :=
   le_antisymm (le_sInf fun _ h => tsub_le_iff_right.mpr h) <| sInf_le <| mem_setOf.2 le_tsub_add
 
 /-- This is a special case of `WithTop.coe_sub` in the `ENNReal` namespace -/
-@[simp] theorem coe_sub : (↑(r - p) : ℝ≥0∞) = ↑r - ↑p := WithTop.coe_sub
+@[simp, norm_cast] theorem coe_sub : (↑(r - p) : ℝ≥0∞) = ↑r - ↑p := WithTop.coe_sub
 
 /-- This is a special case of `WithTop.top_sub_coe` in the `ENNReal` namespace -/
 @[simp] theorem top_sub_coe : ∞ - ↑r = ∞ := WithTop.top_sub_coe
 
+@[simp] lemma top_sub (ha : a ≠ ∞) : ∞ - a = ∞ := by lift a to ℝ≥0 using ha; exact top_sub_coe
+
 /-- This is a special case of `WithTop.sub_top` in the `ENNReal` namespace -/
 theorem sub_top : a - ∞ = 0 := WithTop.sub_top
 

Mathlib/Data/Real/ConjExponents.lean

@@ -18,6 +18,8 @@ analysis, especially when dealing with `L^p` spaces.
 * `Real.conjExponent`: Conjugate exponent of a real number.
 * `NNReal.IsConjExponent`: Predicate for two nonnegative real numbers to be conjugate.
 * `NNReal.conjExponent`: Conjugate exponent of a nonnegative real number.
+* `ENNReal.IsConjExponent`: Predicate for two extended nonnegative real numbers to be conjugate.
+* `ENNReal.conjExponent`: Conjugate exponent of an extended nonnegative real number.
 
 ## TODO
 
@@ -27,7 +29,7 @@ analysis, especially when dealing with `L^p` spaces.
 
 noncomputable section
 
-open scoped ENNReal
+open scoped ENNReal NNReal
 
 namespace Real
 
@@ -116,6 +118,8 @@ lemma one_sub_inv_inv (ha₀ : 0 < a) (ha₁ : a < 1) : (1 - a)⁻¹.IsConjExpon
 
 end IsConjExponent
 
+lemma isConjExponent_comm : p.IsConjExponent q ↔ q.IsConjExponent p := ⟨.symm, .symm⟩
+
 lemma isConjExponent_iff_eq_conjExponent (hp : 1 < p) : p.IsConjExponent q ↔ q = p / (p - 1) :=
   ⟨IsConjExponent.conj_eq, fun h ↦ ⟨hp, by field_simp [h]⟩⟩
 
@@ -206,6 +210,8 @@ lemma one_sub_inv_inv (ha₀ : a ≠ 0) (ha₁ : a < 1) : (1 - a)⁻¹.IsConjExp
 
 end IsConjExponent
 
+lemma isConjExponent_comm : p.IsConjExponent q ↔ q.IsConjExponent p := ⟨.symm, .symm⟩
+
 lemma isConjExponent_iff_eq_conjExponent (h : 1 < p) : p.IsConjExponent q ↔ q = p / (p - 1) := by
   rw [← isConjExponent_coe, Real.isConjExponent_iff_eq_conjExponent (mod_cast h), ← coe_inj,
     NNReal.coe_div, NNReal.coe_sub h.le, coe_one]
@@ -220,3 +226,120 @@ protected lemma Real.IsConjExponent.toNNReal {p q : ℝ} (hpq : p.IsConjExponent
   one_lt := by simpa using hpq.one_lt
   inv_add_inv_conj := by rw [← toNNReal_inv, ← toNNReal_inv, ← toNNReal_add hpq.inv_nonneg
     hpq.symm.inv_nonneg, hpq.inv_add_inv_conj, toNNReal_one]
+
+namespace ENNReal
+
+/-- Two extended nonnegative real exponents `p, q` are conjugate and satisfy the equality
+`1/p + 1/q = 1`. This condition shows up in many theorems in analysis, notably related to `L^p`
+norms. Note that we permit one of the exponents to be `∞` and the other `1`. -/
+@[mk_iff]
+structure IsConjExponent (p q : ℝ≥0∞) : Prop where
+  inv_add_inv_conj : p⁻¹ + q⁻¹ = 1
+
+/-- The conjugate exponent of `p` is `q = 1 + (p - 1)⁻¹`, so that `1/p + 1/q = 1`. -/
+noncomputable def conjExponent (p : ℝ≥0∞) : ℝ≥0∞ := 1 + (p - 1)⁻¹
+
+lemma coe_conjExponent {p : ℝ≥0} (hp : 1 < p) : p.conjExponent = conjExponent p := by
+  rw [NNReal.conjExponent, conjExponent]
+  norm_cast
+  rw [← coe_inv (tsub_pos_of_lt hp).ne']
+  norm_cast
+  field_simp [(tsub_pos_of_lt hp).ne']
+  rw [tsub_add_cancel_of_le hp.le]
+
+variable {a b p q : ℝ≥0∞} (h : p.IsConjExponent q)
+
+@[simp, norm_cast] lemma isConjExponent_coe {p q : ℝ≥0} :
+    IsConjExponent p q ↔ p.IsConjExponent q := by
+  simp only [isConjExponent_iff, NNReal.isConjExponent_iff]
+  refine ⟨fun h ↦ ⟨?_, ?_⟩, ?_⟩
+  · simpa using (ENNReal.lt_add_right (fun hp ↦ by simp [hp] at h) <| by simp).trans_eq h
+  · rw [← coe_inv, ← coe_inv] at h
+    norm_cast at h
+    all_goals rintro rfl; simp at h
+  · rintro ⟨hp, h⟩
+    rw [← coe_inv (zero_lt_one.trans hp).ne', ← coe_inv, ← coe_add, h, coe_one]
+    rintro rfl
+    simp [hp.ne'] at h
+
+alias ⟨_, _root_.NNReal.IsConjExponent.coe_ennreal⟩ := isConjExponent_coe
+
+namespace IsConjExponent
+
+protected lemma conjExponent (hp : 1 ≤ p) : p.IsConjExponent (conjExponent p) := by
+  have : p ≠ 0 := (zero_lt_one.trans_le hp).ne'
+  rw [isConjExponent_iff, conjExponent, add_comm]
+  refine (AddLECancellable.eq_tsub_iff_add_eq_of_le (α := ℝ≥0∞) (by simpa) (by simpa)).1 ?_
+  rw [inv_eq_iff_eq_inv]
+  obtain rfl | hp₁ := hp.eq_or_lt
+  · simp
+  obtain rfl | hp := eq_or_ne p ∞
+  · simp
+  calc
+    1 + (p - 1)⁻¹ = (p - 1 + 1) / (p - 1) := by
+      rw [ENNReal.add_div, ENNReal.div_self ((tsub_pos_of_lt hp₁).ne') (sub_ne_top hp), one_div]
+    _ = (1 - p⁻¹)⁻¹ := by
+      rw [tsub_add_cancel_of_le, ← inv_eq_iff_eq_inv, div_eq_mul_inv, ENNReal.mul_inv, inv_inv,
+        ENNReal.mul_sub, ENNReal.inv_mul_cancel, mul_one] <;> simp [*]
+
+section
+include h
+
+@[symm]
+protected lemma symm : q.IsConjExponent p where
+  inv_add_inv_conj := by simpa [add_comm] using h.inv_add_inv_conj
+
+lemma one_le : 1 ≤ p := ENNReal.inv_le_one.1 <| by
+  rw [← add_zero p⁻¹, ← h.inv_add_inv_conj]; gcongr; positivity
+
+lemma pos : 0 < p := zero_lt_one.trans_le h.one_le
+lemma ne_zero : p ≠ 0 := h.pos.ne'
+
+lemma one_sub_inv : 1 - p⁻¹ = q⁻¹ :=
+  ENNReal.sub_eq_of_eq_add_rev' one_ne_top h.inv_add_inv_conj.symm
+
+lemma conjExponent_eq : conjExponent p = q := by
+  have hp : 1 ≤ p := h.one_le
+  have : p⁻¹ ≠ ∞ := by simpa using h.ne_zero
+  simpa [ENNReal.add_right_inj, *] using
+    (IsConjExponent.conjExponent hp).inv_add_inv_conj.trans h.inv_add_inv_conj.symm
+
+lemma conj_eq : q = 1 + (p - 1)⁻¹ := h.conjExponent_eq.symm
+
+lemma mul_eq_add : p * q = p + q := by
+  obtain rfl | hp := eq_or_ne p ∞
+  · simp [h.symm.ne_zero]
+  obtain rfl | hq := eq_or_ne q ∞
+  · simp [h.ne_zero]
+  rw [← mul_one (_ * _), ← h.inv_add_inv_conj, mul_add, mul_right_comm,
+    ENNReal.mul_inv_cancel h.ne_zero hp, one_mul, mul_assoc,
+    ENNReal.mul_inv_cancel h.symm.ne_zero hq, mul_one, add_comm]
+
+lemma div_conj_eq_sub_one : p / q = p - 1 := by
+  obtain rfl | hq := eq_or_ne q ∞
+  · simp [h.symm.conj_eq]
+  refine ENNReal.eq_sub_of_add_eq one_ne_top ?_
+  rw [← ENNReal.div_self h.symm.ne_zero hq, ← ENNReal.add_div, ← h.mul_eq_add, mul_div_assoc,
+    ENNReal.div_self h.symm.ne_zero hq, mul_one]
+
+end
+
+protected lemma inv_inv (hab : a + b = 1) : a⁻¹.IsConjExponent b⁻¹ where
+  inv_add_inv_conj := by simpa only [inv_inv] using hab
+
+lemma inv_one_sub_inv (ha : a ≤ 1) : a⁻¹.IsConjExponent (1 - a)⁻¹ :=
+  .inv_inv <| add_tsub_cancel_of_le ha
+
+lemma one_sub_inv_inv (ha : a ≤ 1) : (1 - a)⁻¹.IsConjExponent a⁻¹ := (inv_one_sub_inv ha).symm
+
+lemma top_one : IsConjExponent ∞ 1 := ⟨by simp⟩
+lemma one_top : IsConjExponent 1 ∞ := ⟨by simp⟩
+
+end IsConjExponent
+
+lemma isConjExponent_comm : p.IsConjExponent q ↔ q.IsConjExponent p := ⟨.symm, .symm⟩
+
+lemma isConjExponent_iff_eq_conjExponent (hp : 1 ≤ p) : p.IsConjExponent q ↔ q = 1 + (p - 1)⁻¹ :=
+  ⟨fun h ↦ h.conj_eq, by rintro rfl; exact .conjExponent hp⟩
+
+end ENNReal