feat: Hölder's inequality for more than 2 functions (#7756)

* From the Sobolev project

Co-authored-by: Heather Macbeth
25316162+hrmacbeth@users.noreply.github.com

---
<!-- The text above the `---` will become the commit message when your
PR is merged. Please leave a blank newline before the `---`, otherwise
GitHub will format the text above it as a title.

To indicate co-authors, include lines at the bottom of the commit
message
(that is, before the `---`) using the following format:

Co-authored-by: Author Name <author@email.com>

Any other comments you want to keep out of the PR commit should go
below the `---`, and placed outside this HTML comment, or else they
will be invisible to reviewers.

If this PR depends on other PRs, please list them below this comment,
using the following format:
- [ ] depends on: #abc [optional extra text]
- [ ] depends on: #xyz [optional extra text]
-->

[![Open in
Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

---------

Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Mathlib/Algebra/BigOperators/Basic.lean

@@ -342,6 +342,10 @@ theorem prod_insert_one [DecidableEq α] (h : f a = 1) : ∏ x in insert a s, f
 #align finset.prod_insert_one Finset.prod_insert_one
 #align finset.sum_insert_zero Finset.sum_insert_zero
 
+@[to_additive]
+theorem prod_insert_div {M : Type*} [CommGroup M] [DecidableEq α] (ha : a ∉ s) {f : α → M} :
+    (∏ x in insert a s, f x) / f a = ∏ x in s, f x := by simp [ha]
+
 @[to_additive (attr := simp)]
 theorem prod_singleton (f : α → β) (a : α) : ∏ x in singleton a, f x = f a :=
   Eq.trans fold_singleton <| mul_one _

Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean

@@ -587,6 +587,12 @@ theorem coe_mul_rpow (x y : ℝ≥0) (z : ℝ) : ((x : ℝ≥0∞) * y) ^ z = (x
   mul_rpow_of_ne_top coe_ne_top coe_ne_top z
 #align ennreal.coe_mul_rpow ENNReal.coe_mul_rpow
 
+theorem prod_coe_rpow {ι} (s : Finset ι) (f : ι → ℝ≥0) (r : ℝ) :
+    ∏ i in s, (f i : ℝ≥0∞) ^ r = ((∏ i in s, f i : ℝ≥0) : ℝ≥0∞) ^ r := by
+  induction s using Finset.induction
+  case empty => simp
+  case insert i s hi ih => simp_rw [prod_insert hi, ih, ← coe_mul_rpow, coe_mul]
+
 theorem mul_rpow_of_ne_zero {x y : ℝ≥0∞} (hx : x ≠ 0) (hy : y ≠ 0) (z : ℝ) :
     (x * y) ^ z = x ^ z * y ^ z := by simp [*, mul_rpow_eq_ite]
 #align ennreal.mul_rpow_of_ne_zero ENNReal.mul_rpow_of_ne_zero
@@ -595,6 +601,21 @@ theorem mul_rpow_of_nonneg (x y : ℝ≥0∞) {z : ℝ} (hz : 0 ≤ z) : (x * y)
   simp [hz.not_lt, mul_rpow_eq_ite]
 #align ennreal.mul_rpow_of_nonneg ENNReal.mul_rpow_of_nonneg
 
+theorem prod_rpow_of_ne_top {ι} {s : Finset ι} {f : ι → ℝ≥0∞} (hf : ∀ i ∈ s, f i ≠ ∞) (r : ℝ) :
+    ∏ i in s, f i ^ r = (∏ i in s, f i) ^ r := by
+  induction s using Finset.induction
+  case empty => simp
+  case insert i s hi ih =>
+    have h2f : ∀ i ∈ s, f i ≠ ∞ := fun i hi ↦ hf i <| mem_insert_of_mem hi
+    rw [prod_insert hi, prod_insert hi, ih h2f, ← mul_rpow_of_ne_top <| hf i <| mem_insert_self ..]
+    apply prod_lt_top h2f |>.ne
+
+theorem prod_rpow_of_nonneg {ι} {s : Finset ι} {f : ι → ℝ≥0∞} {r : ℝ} (hr : 0 ≤ r) :
+    ∏ i in s, f i ^ r = (∏ i in s, f i) ^ r := by
+  induction s using Finset.induction
+  case empty => simp
+  case insert i s hi ih => simp_rw [prod_insert hi, ih, ← mul_rpow_of_nonneg _ _ hr]
+
 theorem inv_rpow (x : ℝ≥0∞) (y : ℝ) : x⁻¹ ^ y = (x ^ y)⁻¹ := by
   rcases eq_or_ne y 0 with (rfl | hy); · simp only [rpow_zero, inv_one]
   replace hy := hy.lt_or_lt

Mathlib/Data/Finset/Option.lean

@@ -75,6 +75,10 @@ theorem mem_insertNone {s : Finset α} : ∀ {o : Option α}, o ∈ insertNone s
 theorem some_mem_insertNone {s : Finset α} {a : α} : some a ∈ insertNone s ↔ a ∈ s := by simp
 #align finset.some_mem_insert_none Finset.some_mem_insertNone
 
+lemma none_mem_insertNone {s : Finset α} : none ∈ insertNone s := by simp
+
+lemma insertNone_nonempty {s : Finset α} : insertNone s |>.Nonempty := ⟨none, none_mem_insertNone⟩
+
 @[simp]
 theorem card_insertNone (s : Finset α) : s.insertNone.card = s.card + 1 := by simp [insertNone]
 #align finset.card_insert_none Finset.card_insertNone

Mathlib/MeasureTheory/Integral/MeanInequalities.lean

@@ -24,6 +24,12 @@ and `α → (E)NNReal` functions in two cases,
 * `ENNReal.lintegral_mul_le_Lp_mul_Lq` : ℝ≥0∞ functions,
 * `NNReal.lintegral_mul_le_Lp_mul_Lq`  : ℝ≥0 functions.
 
+`ENNReal.lintegral_mul_norm_pow_le` is a variant where the exponents are not reciprocals:
+`∫ (f ^ p * g ^ q) ∂μ ≤ (∫ f ∂μ) ^ p * (∫ g ∂μ) ^ q` where `p, q ≥ 0` and `p + q = 1`.
+`ENNReal.lintegral_prod_norm_pow_le` generalizes this to a finite family of functions:
+`∫ (∏ i, f i ^ p i) ∂μ ≤ ∏ i, (∫ f i ∂μ) ^ p i` when the `p` is a collection
+of nonnegative weights with sum 1.
+
 Minkowski's inequality for the Lebesgue integral of measurable functions with `ℝ≥0∞` values:
 we prove `(∫ (f + g)^p ∂μ) ^ (1/p) ≤ (∫ f^p ∂μ) ^ (1/p) + (∫ g^p ∂μ) ^ (1/p)` for `1 ≤ p`.
 -/
@@ -48,7 +54,7 @@ only to prove the more general results:
 
 noncomputable section
 
-open Classical BigOperators NNReal ENNReal MeasureTheory
+open Classical BigOperators NNReal ENNReal MeasureTheory Finset
 
 set_option linter.uppercaseLean3 false
 
@@ -175,6 +181,101 @@ theorem lintegral_mul_le_Lp_mul_Lq (μ : Measure α) {p q : ℝ} (hpq : p.IsConj
   exact ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top hpq hf hf_top hg_top hf_zero hg_zero
 #align ennreal.lintegral_mul_le_Lp_mul_Lq ENNReal.lintegral_mul_le_Lp_mul_Lq
 
+/-- A different formulation of Hölder's inequality for two functions, with two exponents that sum to
+1, instead of reciprocals of  -/
+theorem lintegral_mul_norm_pow_le {α} [MeasurableSpace α] {μ : Measure α}
+    {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
+    {p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) (hpq : p + q = 1) :
+    ∫⁻ a, f a ^ p * g a ^ q ∂μ ≤ (∫⁻ a, f a ∂μ) ^ p * (∫⁻ a, g a ∂μ) ^ q := by
+  rcases hp.eq_or_lt with rfl|hp
+  · rw [zero_add] at hpq
+    simp [hpq]
+  rcases hq.eq_or_lt with rfl|hq
+  · rw [add_zero] at hpq
+    simp [hpq]
+  have h2p : 1 < 1 / p := by
+    rw [one_div]
+    apply one_lt_inv hp
+    linarith
+  have h2pq : 1 / (1 / p) + 1 / (1 / q) = 1 := by
+    simp [hp.ne', hq.ne', hpq]
+  have := ENNReal.lintegral_mul_le_Lp_mul_Lq μ ⟨h2p, h2pq⟩ (hf.pow_const p) (hg.pow_const q)
+  simpa [← ENNReal.rpow_mul, hp.ne', hq.ne'] using this
+
+/-- A version of Hölder with multiple arguments -/
+theorem lintegral_prod_norm_pow_le {α ι : Type*} [MeasurableSpace α] {μ : Measure α}
+    (s : Finset ι) {f : ι → α → ℝ≥0∞} (hf : ∀ i ∈ s, AEMeasurable (f i) μ)
+    {p : ι → ℝ} (hp : ∑ i in s, p i = 1) (h2p : ∀ i ∈ s, 0 ≤ p i) :
+    ∫⁻ a, ∏ i in s, f i a ^ p i ∂μ ≤ ∏ i in s, (∫⁻ a, f i a ∂μ) ^ p i := by
+  induction s using Finset.induction generalizing p
+  case empty =>
+    simp at hp
+  case insert i₀ s hi₀ ih =>
+    rcases eq_or_ne (p i₀) 1 with h2i₀|h2i₀
+    · simp [hi₀]
+      have h2p : ∀ i ∈ s, p i = 0 := by
+        simpa [hi₀, h2i₀, sum_eq_zero_iff_of_nonneg (fun i hi ↦ h2p i <| mem_insert_of_mem hi)]
+          using hp
+      calc ∫⁻ a, f i₀ a ^ p i₀ * ∏ i in s, f i a ^ p i ∂μ
+          = ∫⁻ a, f i₀ a ^ p i₀ * ∏ i in s, 1 ∂μ := by
+            congr! 3 with x
+            apply prod_congr rfl fun i hi ↦ by rw [h2p i hi, ENNReal.rpow_zero]
+        _ ≤ (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * ∏ i in s, 1 := by simp [h2i₀]
+        _ = (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * ∏ i in s, (∫⁻ a, f i a ∂μ) ^ p i := by
+            congr 1
+            apply prod_congr rfl fun i hi ↦ by rw [h2p i hi, ENNReal.rpow_zero]
+    · have hpi₀ : 0 ≤ 1 - p i₀ := by
+        simp_rw [sub_nonneg, ← hp, single_le_sum h2p (mem_insert_self ..)]
+      have h2pi₀ : 1 - p i₀ ≠ 0 := by
+        rwa [sub_ne_zero, ne_comm]
+      let q := fun i ↦ p i / (1 - p i₀)
+      have hq : ∑ i in s, q i = 1 := by
+        rw [← Finset.sum_div, ← sum_insert_sub hi₀, hp, div_self h2pi₀]
+      have h2q : ∀ i ∈ s, 0 ≤ q i :=
+        fun i hi ↦ div_nonneg (h2p i <| mem_insert_of_mem hi) hpi₀
+      calc ∫⁻ a, ∏ i in insert i₀ s, f i a ^ p i ∂μ
+          = ∫⁻ a, f i₀ a ^ p i₀ * ∏ i in s, f i a ^ p i ∂μ := by simp [hi₀]
+        _ = ∫⁻ a, f i₀ a ^ p i₀ * (∏ i in s, f i a ^ q i) ^ (1 - p i₀) ∂μ := by
+            simp [← ENNReal.prod_rpow_of_nonneg hpi₀, ← ENNReal.rpow_mul,
+              div_mul_cancel (h := h2pi₀)]
+        _ ≤ (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * (∫⁻ a, ∏ i in s, f i a ^ q i ∂μ) ^ (1 - p i₀) := by
+            apply ENNReal.lintegral_mul_norm_pow_le
+            · exact hf i₀ <| mem_insert_self ..
+            · exact s.aemeasurable_prod <| fun i hi ↦ (hf i <| mem_insert_of_mem hi).pow_const _
+            · exact h2p i₀ <| mem_insert_self ..
+            · exact hpi₀
+            · apply add_sub_cancel'_right
+        _ ≤ (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * (∏ i in s, (∫⁻ a, f i a ∂μ) ^ q i) ^ (1 - p i₀) := by
+            gcongr -- behavior of gcongr is heartbeat-dependent, which makes code really fragile...
+            exact ih (fun i hi ↦ hf i <| mem_insert_of_mem hi) hq h2q
+        _ = (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * ∏ i in s, (∫⁻ a, f i a ∂μ) ^ p i := by
+            simp [← ENNReal.prod_rpow_of_nonneg hpi₀, ← ENNReal.rpow_mul,
+              div_mul_cancel (h := h2pi₀)]
+        _ = ∏ i in insert i₀ s, (∫⁻ a, f i a ∂μ) ^ p i := by simp [hi₀]
+
+/-- A version of Hölder with multiple arguments, one of which plays a distinguished role. -/
+theorem lintegral_mul_prod_norm_pow_le {α ι : Type*} [MeasurableSpace α] {μ : Measure α}
+    (s : Finset ι) {g : α →  ℝ≥0∞} {f : ι → α → ℝ≥0∞} (hg : AEMeasurable g μ)
+    (hf : ∀ i ∈ s, AEMeasurable (f i) μ) (q : ℝ) {p : ι → ℝ} (hpq : q + ∑ i in s, p i = 1)
+    (hq :  0 ≤ q) (hp : ∀ i ∈ s, 0 ≤ p i) :
+    ∫⁻ a, g a ^ q * ∏ i in s, f i a ^ p i ∂μ ≤
+      (∫⁻ a, g a ∂μ) ^ q * ∏ i in s, (∫⁻ a, f i a ∂μ) ^ p i := by
+  suffices
+    ∫⁻ t, ∏ j in insertNone s, Option.elim j (g t) (fun j ↦ f j t) ^ Option.elim j q p ∂μ
+    ≤ ∏ j in insertNone s, (∫⁻ t, Option.elim j (g t) (fun j ↦ f j t) ∂μ) ^ Option.elim j q p by
+    simpa using this
+  refine ENNReal.lintegral_prod_norm_pow_le _ ?_ ?_ ?_
+  · rintro (_|i) hi
+    · exact hg
+    · refine hf i ?_
+      simpa using hi
+  · simp_rw [sum_insertNone, Option.elim]
+    exact hpq
+  · rintro (_|i) hi
+    · exact hq
+    · refine hp i ?_
+      simpa using hi
+
 theorem lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top {p : ℝ} {f g : α → ℝ≥0∞}
     (hf : AEMeasurable f μ) (hf_top : (∫⁻ a, f a ^ p ∂μ) < ⊤) (hg_top : (∫⁻ a, g a ^ p ∂μ) < ⊤)
     (hp1 : 1 ≤ p) : (∫⁻ a, (f + g) a ^ p ∂μ) < ⊤ := by