From e18358e062ed10bbe12c4c7b9c078dcd26fe12f1 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Thu, 12 Feb 2026 14:07:32 -0600 Subject: [PATCH 1/3] =?UTF-8?q?feat:=20generalize=20H=C3=B6lder's=20inequa?= =?UTF-8?q?lity=20for=20sums=20to=20`Real.HolderTriple`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/Analysis/MeanInequalities.lean | 191 ++++++++++++++++++++----- Mathlib/Data/Real/ConjExponents.lean | 8 ++ 2 files changed, 160 insertions(+), 39 deletions(-) diff --git a/Mathlib/Analysis/MeanInequalities.lean b/Mathlib/Analysis/MeanInequalities.lean index b78048b10d80d6..854e585302ce6c 100644 --- a/Mathlib/Analysis/MeanInequalities.lean +++ b/Mathlib/Analysis/MeanInequalities.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2019 Yury Kudryashov. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Yury Kudryashov, Sébastien Gouëzel, Rémy Degenne +Authors: Yury Kudryashov, Sébastien Gouëzel, Rémy Degenne, Jireh Loreaux -/ module @@ -494,14 +494,42 @@ theorem inner_le_Lp_mul_Lq (f g : ι → ℝ≥0) {p q : ℝ} (hpq : p.HolderCon suffices (∑ i ∈ s, f' i * g' i) ≤ 1 by simp_rw [f', g', div_mul_div_comm, ← sum_div] at this rwa [div_le_iff₀, one_mul] at this - -- TODO: We are missing a positivity extension here - exact mul_pos (rpow_pos hf) (rpow_pos hg) + positivity refine inner_le_Lp_mul_Lp_of_norm_le_one s f' g' hpq (le_of_eq ?_) (le_of_eq ?_) · simp_rw [f', div_rpow, ← sum_div, ← rpow_mul, one_div, inv_mul_cancel₀ hpq.ne_zero, rpow_one, div_self hf.ne'] · simp_rw [g', div_rpow, ← sum_div, ← rpow_mul, one_div, inv_mul_cancel₀ hpq.symm.ne_zero, rpow_one, div_self hg.ne'] +/-- **Hölder inequality**: The (`r`-power of the) `L^r` norm of two functions is bounded by the +product of (the `r`-powers of) their `L^p` and `L^q` norms when `p`, `q`, and `r` form a +`Real.HolderTriple`. -/ +theorem Lr_rpow_le_Lp_mul_Lq (f g : ι → ℝ≥0) {p q r : ℝ} (hpqr : p.HolderTriple q r) : + ∑ i ∈ s, (f i * g i) ^ r ≤ (∑ i ∈ s, f i ^ p) ^ (r / p) * (∑ i ∈ s, g i ^ q) ^ (r / q) := by + have := hpqr.holderConjugate_div_div + have hp := hpqr.pos + have hq := hpqr.symm.pos + have hr := hpqr.pos' + calc ∑ i ∈ s, (f i * g i) ^ r + _ = ∑ i ∈ s, (f i) ^ r * (g i) ^ r := s.sum_congr rfl fun i hi ↦ mul_rpow .. + _ ≤ (∑ i ∈ s, f i ^ p) ^ (r / p) * (∑ i ∈ s, g i ^ q) ^ (r / q) := by + apply inner_le_Lp_mul_Lq s _ _ this |>.trans_eq + congr! 2 + all_goals try simp only [fieldEq] + all_goals + refine s.sum_congr rfl fun i hi ↦ by simp [← rpow_mul, ← mul_div_assoc, hr.ne'] + +/-- **Hölder inequality**: The `L^r` norm of two functions is bounded by the +product of their `L^p` and `L^q` norms when `p`, `q`, and `r` form a `Real.HolderTriple`. -/ +theorem Lr_le_Lp_mul_Lq (f g : ι → ℝ≥0) {p q r : ℝ} (hpqr : p.HolderTriple q r) : + (∑ i ∈ s, (f i * g i) ^ r) ^ (1 / r) ≤ + (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q) := by + convert rpow_le_rpow_iff (inv_eq_one_div r ▸ inv_pos.mpr hpqr.pos' : 0 < 1 / r) |>.mpr <| + Lr_rpow_le_Lp_mul_Lq s f g hpqr using 1 + have hr := hpqr.pos'.ne' + simp only [← rpow_mul, mul_rpow] + field_simp + /-- **Weighted Hölder inequality**. -/ lemma inner_le_weight_mul_Lp (s : Finset ι) {p : ℝ} (hp : 1 ≤ p) (w f : ι → ℝ≥0) : ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ := by @@ -520,38 +548,70 @@ lemma inner_le_weight_mul_Lp (s : Finset ι) {p : ℝ} (hp : 1 ≤ p) (w f : ι have hp₁ : 1 - p⁻¹ ≠ 0 := by simp [sub_eq_zero, hp.ne'] simp [mul_rpow, div_inv_eq_mul, one_mul, one_div, hp₀, hp₁] -/-- **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. A version for `NNReal`-valued -functions. For an alternative version, convenient if the infinite sums are already expressed as -`p`-th powers, see `inner_le_Lp_mul_Lq_hasSum`. -/ -theorem inner_le_Lp_mul_Lq_tsum {f g : ι → ℝ≥0} {p q : ℝ} (hpq : p.HolderConjugate q) - (hf : Summable fun i => f i ^ p) (hg : Summable fun i => g i ^ q) : - (Summable fun i => f i * g i) ∧ - ∑' i, f i * g i ≤ (∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q) := by +/-- **Hölder inequality**: The (`r`-power of the) `L^r` norm of two functions is bounded by the +product of (the `r`-powers of) their `L^p` and `L^q` norms when `p`, `q`, and `r` form a +`Real.HolderTriple`. A version for `NNReal`-valued functions. For an alternative version, +convenient if the infinite sums are already expressed as powers, see `inner_le_Lp_mul_Lq_hasSum`. -/ +theorem summable_and_Lr_rpow_le_Lp_mul_Lq_tsum {f g : ι → ℝ≥0} {p q r : ℝ} + (hpqr : p.HolderTriple q r) (hf : Summable fun i => f i ^ p) (hg : Summable fun i => g i ^ q) : + (Summable fun i => (f i * g i) ^ r) ∧ + ∑' i, (f i * g i) ^ r ≤ (∑' i, f i ^ p) ^ (r / p) * (∑' i, g i ^ q) ^ (r / q) := by have H₁ : ∀ s : Finset ι, - ∑ i ∈ s, f i * g i ≤ (∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q) := by + ∑ i ∈ s, (f i * g i) ^ r ≤ (∑' i, f i ^ p) ^ (r / p) * (∑' i, g i ^ q) ^ (r / q) := by intro s - refine le_trans (inner_le_Lp_mul_Lq s f g hpq) (mul_le_mul ?_ ?_ bot_le bot_le) - · rw [NNReal.rpow_le_rpow_iff (one_div_pos.mpr hpq.pos)] + obtain ⟨hp, hq, hr⟩ := hpqr.all_pos + refine le_trans (Lr_rpow_le_Lp_mul_Lq s f g hpqr) (mul_le_mul ?_ ?_ bot_le bot_le) + · rw [NNReal.rpow_le_rpow_iff (by positivity)] exact hf.sum_le_tsum _ (fun _ _ => zero_le _) - · rw [NNReal.rpow_le_rpow_iff (one_div_pos.mpr hpq.symm.pos)] + · rw [NNReal.rpow_le_rpow_iff (by positivity)] exact hg.sum_le_tsum _ (fun _ _ => zero_le _) - have bdd : BddAbove (Set.range fun s => ∑ i ∈ s, f i * g i) := by - refine ⟨(∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q), ?_⟩ + have bdd : BddAbove (Set.range fun s => ∑ i ∈ s, (f i * g i) ^ r) := by + refine ⟨(∑' i, f i ^ p) ^ (r / p) * (∑' i, g i ^ q) ^ (r / q), ?_⟩ rintro a ⟨s, rfl⟩ exact H₁ s have H₂ : Summable _ := (hasSum_of_isLUB _ (isLUB_ciSup bdd)).summable exact ⟨H₂, H₂.tsum_le_of_sum_le H₁⟩ +/-- **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. A version for `NNReal`-valued +functions. For an alternative version, convenient if the infinite sums are already expressed as +`p`-th powers, see `inner_le_Lp_mul_Lq_hasSum`. -/ +theorem summable_and_inner_le_Lp_mul_Lq_tsum {f g : ι → ℝ≥0} {p q : ℝ} (hpq : p.HolderConjugate q) + (hf : Summable fun i => f i ^ p) (hg : Summable fun i => g i ^ q) : + (Summable fun i => f i * g i) ∧ + ∑' i, f i * g i ≤ (∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q) := by + simpa using summable_and_Lr_rpow_le_Lp_mul_Lq_tsum hpq hf hg + +theorem summable_mul_rpow_of_Lp_Lq {f g : ι → ℝ≥0} {p q r : ℝ} (hpqr : p.HolderTriple q r) + (hf : Summable fun i => f i ^ p) (hg : Summable fun i => g i ^ q) : + Summable fun i => (f i * g i) ^ r := + (summable_and_Lr_rpow_le_Lp_mul_Lq_tsum hpqr hf hg).1 + theorem summable_mul_of_Lp_Lq {f g : ι → ℝ≥0} {p q : ℝ} (hpq : p.HolderConjugate q) (hf : Summable fun i => f i ^ p) (hg : Summable fun i => g i ^ q) : Summable fun i => f i * g i := - (inner_le_Lp_mul_Lq_tsum hpq hf hg).1 + (summable_and_inner_le_Lp_mul_Lq_tsum hpq hf hg).1 -theorem inner_le_Lp_mul_Lq_tsum' {f g : ι → ℝ≥0} {p q : ℝ} (hpq : p.HolderConjugate q) +theorem Lr_rpow_le_Lp_mul_Lq_tsum {f g : ι → ℝ≥0} {p q r : ℝ} (hpqr : p.HolderTriple q r) + (hf : Summable fun i => f i ^ p) (hg : Summable fun i => g i ^ q) : + ∑' i, (f i * g i) ^ r ≤ (∑' i, f i ^ p) ^ (r / p) * (∑' i, g i ^ q) ^ (r / q) := + (summable_and_Lr_rpow_le_Lp_mul_Lq_tsum hpqr hf hg).2 + +theorem Lr_le_Lp_mul_Lq_tsum {f g : ι → ℝ≥0} {p q r : ℝ} (hpqr : p.HolderTriple q r) + (hf : Summable fun i => f i ^ p) (hg : Summable fun i => g i ^ q) : + (∑' i, (f i * g i) ^ r) ^ (1 / r) ≤ (∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q) := by + convert rpow_le_rpow_iff (inv_eq_one_div r ▸ inv_pos.mpr hpqr.pos') |>.mpr <| + Lr_rpow_le_Lp_mul_Lq_tsum hpqr hf hg + have hr := hpqr.pos'.ne' + simp only [← rpow_mul, mul_rpow] + field_simp + +theorem inner_le_Lp_mul_Lq_tsum {f g : ι → ℝ≥0} {p q : ℝ} (hpq : p.HolderConjugate q) (hf : Summable fun i => f i ^ p) (hg : Summable fun i => g i ^ q) : ∑' i, f i * g i ≤ (∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q) := - (inner_le_Lp_mul_Lq_tsum hpq hf hg).2 + (summable_and_inner_le_Lp_mul_Lq_tsum hpq hf hg).2 + +@[deprecated (since := "2026-02-12")] alias inner_le_Lp_mul_Lq_tsum' := inner_le_Lp_mul_Lq_tsum /-- **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. A version for `NNReal`-valued @@ -560,7 +620,7 @@ functions. For an alternative version, convenient if the infinite sums are not a theorem inner_le_Lp_mul_Lq_hasSum {f g : ι → ℝ≥0} {A B : ℝ≥0} {p q : ℝ} (hpq : p.HolderConjugate q) (hf : HasSum (fun i => f i ^ p) (A ^ p)) (hg : HasSum (fun i => g i ^ q) (B ^ q)) : ∃ C, C ≤ A * B ∧ HasSum (fun i => f i * g i) C := by - obtain ⟨H₁, H₂⟩ := inner_le_Lp_mul_Lq_tsum hpq hf.summable hg.summable + obtain ⟨H₁, H₂⟩ := summable_and_inner_le_Lp_mul_Lq_tsum hpq hf.summable hg.summable have hA : A = (∑' i : ι, f i ^ p) ^ (1 / p) := by rw [hf.tsum_eq, rpow_inv_rpow_self hpq.ne_zero] have hB : B = (∑' i : ι, g i ^ q) ^ (1 / q) := by rw [hg.tsum_eq, rpow_inv_rpow_self hpq.symm.ne_zero] @@ -680,19 +740,22 @@ end NNReal namespace Real -variable (f g : ι → ℝ) {p q : ℝ} +variable (f g : ι → ℝ) {p q r : ℝ} + +/-- **Hölder inequality**: the sum of (the `r`-powers of) the product of two functions is bounded by +the product of their `L^p` and `L^q` norms when `p`, `q` and `r` form a `Real.HolderTriple`. +Version for sums over finite sets, with real-valued functions. -/ +theorem Lr_rpow_le_Lp_mul_Lq (hpqr : HolderTriple p q r) : + ∑ i ∈ s, |f i * g i| ^ r ≤ (∑ i ∈ s, |f i| ^ p) ^ (r / p) * (∑ i ∈ s, |g i| ^ q) ^ (r / q) := by + simpa using NNReal.coe_le_coe.2 <| NNReal.Lr_rpow_le_Lp_mul_Lq s (fun i ↦ ⟨_, abs_nonneg (f i)⟩) + (fun i ↦ ⟨_, abs_nonneg (g i)⟩) hpqr /-- **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 real-valued functions. -/ theorem inner_le_Lp_mul_Lq (hpq : HolderConjugate p q) : ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) * (∑ i ∈ s, |g i| ^ q) ^ (1 / q) := by - have := - NNReal.coe_le_coe.2 - (NNReal.inner_le_Lp_mul_Lq s (fun i => ⟨_, abs_nonneg (f i)⟩) (fun i => ⟨_, abs_nonneg (g i)⟩) - hpq) - push_cast at this - refine le_trans (sum_le_sum fun i _ => ?_) this + refine le_trans (sum_le_sum fun i _ ↦ ?_) (by simpa using Lr_rpow_le_Lp_mul_Lq s f g hpq) simp only [← abs_mul, le_abs_self] /-- For `1 ≤ p`, the `p`-th power of the sum of `f i` is bounded above by a constant times the @@ -730,6 +793,18 @@ theorem inner_le_Lp_mul_Lq_of_nonneg (hpq : HolderConjugate p q) (hf : ∀ i ∈ convert inner_le_Lp_mul_Lq s f g hpq using 3 <;> apply sum_congr rfl <;> intro i hi <;> simp only [abs_of_nonneg, hf i hi, hg i hi] +/-- **Hölder inequality**: the sum of (the `r`-power of) the product of two functions is bounded +by (the `r`-power of) the product of their `L^p` and `L^q` norms, when `p`, `q`, `r` form a +`Real.HolderTriple`. -/ +theorem Lr_rpow_le_Lp_mul_Lq_of_nonneg {ι : Type*} (s : Finset ι) {f g : ι → ℝ} {p q r : ℝ} + (hpqr : p.HolderTriple q r) (hf : ∀ i ∈ s, 0 ≤ f i) (hg : ∀ i ∈ s, 0 ≤ g i) : + ∑ i ∈ s, (f i * g i) ^ r ≤ (∑ i ∈ s, f i ^ p) ^ (r / p) * (∑ i ∈ s, g i ^ q) ^ (r / q) := by + convert Lr_rpow_le_Lp_mul_Lq s f g hpqr using 3 with i hi + · rw [abs_of_nonneg (mul_nonneg (hf i hi) (hg i hi))] + all_goals + congr! with i hi + exact Eq.symm (abs_of_nonneg (by grind)) + /-- **Weighted Hölder inequality**. -/ lemma inner_le_weight_mul_Lp_of_nonneg (s : Finset ι) {p : ℝ} (hp : 1 ≤ p) (w f : ι → ℝ) (hw : ∀ i, 0 ≤ w i) (hf : ∀ i, 0 ≤ f i) : @@ -752,30 +827,68 @@ lemma compact_inner_le_weight_mul_Lp_of_nonneg (s : Finset ι) {p : ℝ} (hp : 1 · exact sum_nonneg fun i _ ↦ by have := hw i; have := hf i; positivity · exact sum_nonneg fun i _ ↦ by have := hw i; positivity +/-- **Hölder inequality**: the sum of (the `r`-powers of) two functions is bounded by the product +of (the `r`-powers of) their `L^p` and `L^q` norms when `p`, `q` and `r` form a `Real.HolderTriple`. +A version for `ℝ`-valued functions. -/ +theorem summable_and_Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg (hpqr : p.HolderTriple q r) + (hf : ∀ i, 0 ≤ f i) (hg : ∀ i, 0 ≤ g i) (hf_sum : Summable fun i => f i ^ p) + (hg_sum : Summable fun i => g i ^ q) : + (Summable fun i => (f i * g i) ^ r) ∧ + ∑' i, (f i * g i) ^ r ≤ (∑' i, f i ^ p) ^ (r / p) * (∑' i, g i ^ q) ^ (r / q) := by + lift f to ι → ℝ≥0 using hf + lift g to ι → ℝ≥0 using hg + -- After https://github.com/leanprover/lean4/pull/2734, `norm_cast` needs help with beta reduction. + beta_reduce at * + norm_cast at * + exact NNReal.summable_and_Lr_rpow_le_Lp_mul_Lq_tsum hpqr hf_sum hg_sum + /-- **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. A version for `ℝ`-valued functions. For an alternative version, convenient if the infinite sums are already expressed as `p`-th powers, see `inner_le_Lp_mul_Lq_hasSum_of_nonneg`. -/ -theorem inner_le_Lp_mul_Lq_tsum_of_nonneg (hpq : p.HolderConjugate q) (hf : ∀ i, 0 ≤ f i) - (hg : ∀ i, 0 ≤ g i) (hf_sum : Summable fun i => f i ^ p) (hg_sum : Summable fun i => g i ^ q) : +theorem summable_and_inner_le_Lp_mul_Lq_tsum_of_nonneg (hpq : p.HolderConjugate q) + (hf : ∀ i, 0 ≤ f i) (hg : ∀ i, 0 ≤ g i) (hf_sum : Summable fun i => f i ^ p) + (hg_sum : Summable fun i => g i ^ q) : (Summable fun i => f i * g i) ∧ ∑' i, f i * g i ≤ (∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q) := by - lift f to ι → ℝ≥0 using hf - lift g to ι → ℝ≥0 using hg - -- After https://github.com/leanprover/lean4/pull/2734, `norm_cast` needs help with beta reduction. - beta_reduce at * - norm_cast at * - exact NNReal.inner_le_Lp_mul_Lq_tsum hpq hf_sum hg_sum + simpa using summable_and_Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg hpq hf hg hf_sum hg_sum + +theorem summable_Lr_of_Lp_Lq_of_nonneg (hpqr : p.HolderTriple q r) (hf : ∀ i, 0 ≤ f i) + (hg : ∀ i, 0 ≤ g i) (hf_sum : Summable fun i => f i ^ p) (hg_sum : Summable fun i => g i ^ q) : + Summable fun i => (f i * g i) ^ r := + (summable_and_Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg hpqr hf hg hf_sum hg_sum).1 theorem summable_mul_of_Lp_Lq_of_nonneg (hpq : p.HolderConjugate q) (hf : ∀ i, 0 ≤ f i) (hg : ∀ i, 0 ≤ g i) (hf_sum : Summable fun i => f i ^ p) (hg_sum : Summable fun i => g i ^ q) : Summable fun i => f i * g i := - (inner_le_Lp_mul_Lq_tsum_of_nonneg hpq hf hg hf_sum hg_sum).1 + (summable_and_inner_le_Lp_mul_Lq_tsum_of_nonneg hpq hf hg hf_sum hg_sum).1 -theorem inner_le_Lp_mul_Lq_tsum_of_nonneg' (hpq : p.HolderConjugate q) (hf : ∀ i, 0 ≤ f i) +theorem Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg (hpqr : p.HolderTriple q r) (hf : ∀ i, 0 ≤ f i) + (hg : ∀ i, 0 ≤ g i) (hf_sum : Summable fun i => f i ^ p) (hg_sum : Summable fun i => g i ^ q) : + ∑' i, (f i * g i) ^ r ≤ (∑' i, f i ^ p) ^ (r / p) * (∑' i, g i ^ q) ^ (r / q) := + (summable_and_Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg hpqr hf hg hf_sum hg_sum).2 + +theorem Lr_le_Lp_mul_Lq_tsum_of_nonneg (hpqr : p.HolderTriple q r) (hf : ∀ i, 0 ≤ f i) + (hg : ∀ i, 0 ≤ g i) (hf_sum : Summable fun i => f i ^ p) (hg_sum : Summable fun i => g i ^ q) : + (∑' i, (f i * g i) ^ r) ^ (1 / r) ≤ (∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q) := by + -- It's really inconvenient that `positivity` can't use `∀` hypotheses. + have hf' : 0 ≤ ∑' i, f i ^ p := tsum_nonneg fun i ↦ rpow_nonneg (hf i) p + have hg' : 0 ≤ ∑' i, g i ^ q := tsum_nonneg fun i ↦ rpow_nonneg (hg i) q + obtain ⟨hp, hq, hr⟩ := hpqr.all_pos + convert rpow_le_rpow_iff (tsum_nonneg fun i ↦ rpow_nonneg (mul_nonneg (hf i) (hg i)) r) + (by apply mul_nonneg; all_goals apply rpow_nonneg; assumption) + (inv_eq_one_div r ▸ inv_pos.mpr hpqr.pos') |>.mpr <| + Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg hpqr hf hg hf_sum hg_sum using 1 + rw [mul_rpow (rpow_nonneg hf' _) (rpow_nonneg hg' _), ← Real.rpow_mul hg', ← Real.rpow_mul hf'] + field_simp + +theorem inner_le_Lp_mul_Lq_tsum_of_nonneg (hpq : p.HolderConjugate q) (hf : ∀ i, 0 ≤ f i) (hg : ∀ i, 0 ≤ g i) (hf_sum : Summable fun i => f i ^ p) (hg_sum : Summable fun i => g i ^ q) : ∑' i, f i * g i ≤ (∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q) := - (inner_le_Lp_mul_Lq_tsum_of_nonneg hpq hf hg hf_sum hg_sum).2 + (summable_and_inner_le_Lp_mul_Lq_tsum_of_nonneg hpq hf hg hf_sum hg_sum).2 + +@[deprecated (since := "2026-02-12")] +alias inner_le_Lp_mul_Lq_of_nonneg' := inner_le_Lp_mul_Lq_of_nonneg /-- **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. A version for `NNReal`-valued diff --git a/Mathlib/Data/Real/ConjExponents.lean b/Mathlib/Data/Real/ConjExponents.lean index 8ca9a2d1628a3c..06f66035c76433 100644 --- a/Mathlib/Data/Real/ConjExponents.lean +++ b/Mathlib/Data/Real/ConjExponents.lean @@ -108,6 +108,10 @@ theorem one_div_nonneg' : 0 ≤ 1 / r := le_of_lt h.one_div_pos' /-- For `r`, instead of `p` -/ theorem one_div_ne_zero' : 1 / r ≠ 0 := ne_of_gt h.one_div_pos' +/-- useful for introducing all three facts simultaneously within a proof. -/ +@[grind →] +theorem all_pos : 0 < p ∧ 0 < q ∧ 0 < r := ⟨h.pos, h.symm.pos, h.pos'⟩ + lemma inv_eq : r⁻¹ = p⁻¹ + q⁻¹ := h.inv_add_inv_eq_inv.symm lemma one_div_add_one_div : 1 / p + 1 / q = 1 / r := by simpa using h.inv_add_inv_eq_inv lemma one_div_eq : 1 / r = 1 / p + 1 / q := h.one_div_add_one_div.symm @@ -288,6 +292,10 @@ theorem one_div_nonneg' : 0 ≤ 1 / r := le_of_lt h.one_div_pos' /-- For `r`, instead of `p` -/ theorem one_div_ne_zero' : 1 / r ≠ 0 := ne_of_gt h.one_div_pos' +/-- useful for introducing all three facts simultaneously within a proof. -/ +@[grind →] +theorem all_pos : 0 < p ∧ 0 < q ∧ 0 < r := ⟨h.pos, h.symm.pos, h.pos'⟩ + lemma inv_eq : r⁻¹ = p⁻¹ + q⁻¹ := h.inv_add_inv_eq_inv.symm lemma one_div_add_one_div : 1 / p + 1 / q = 1 / r := by exact_mod_cast h.coe.one_div_add_one_div lemma one_div_eq : 1 / r = 1 / p + 1 / q := h.one_div_add_one_div.symm From ed85ab68a5717a4632da9d119f6a464e14839731 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Tue, 17 Mar 2026 08:45:25 -0500 Subject: [PATCH 2/3] Apply suggestions from code review Co-authored-by: Anatole Dedecker --- Mathlib/Analysis/MeanInequalities.lean | 55 ++++++++++++-------------- 1 file changed, 26 insertions(+), 29 deletions(-) diff --git a/Mathlib/Analysis/MeanInequalities.lean b/Mathlib/Analysis/MeanInequalities.lean index 8193b85150a9c1..43e69c2353ca03 100644 --- a/Mathlib/Analysis/MeanInequalities.lean +++ b/Mathlib/Analysis/MeanInequalities.lean @@ -502,26 +502,23 @@ theorem inner_le_Lp_mul_Lq (f g : ι → ℝ≥0) {p q : ℝ} (hpq : p.HolderCon · simp_rw [g', div_rpow, ← sum_div, ← rpow_mul, one_div, inv_mul_cancel₀ hpq.symm.ne_zero, rpow_one, div_self hg.ne'] -/-- **Hölder inequality**: The (`r`-power of the) `L^r` norm of two functions is bounded by the -product of (the `r`-powers of) their `L^p` and `L^q` norms when `p`, `q`, and `r` form a -`Real.HolderTriple`. -/ +/-- **Hölder inequality**: The (`r`-power of the) `L^r` norm of the product of two functions is +bounded by the product of (the `r`-powers of) their `L^p` and `L^q` norms when `p`, `q`, and `r` +form a `Real.HolderTriple`. -/ theorem Lr_rpow_le_Lp_mul_Lq (f g : ι → ℝ≥0) {p q r : ℝ} (hpqr : p.HolderTriple q r) : ∑ i ∈ s, (f i * g i) ^ r ≤ (∑ i ∈ s, f i ^ p) ^ (r / p) * (∑ i ∈ s, g i ^ q) ^ (r / q) := by - have := hpqr.holderConjugate_div_div - have hp := hpqr.pos - have hq := hpqr.symm.pos - have hr := hpqr.pos' - calc ∑ i ∈ s, (f i * g i) ^ r - _ = ∑ i ∈ s, (f i) ^ r * (g i) ^ r := s.sum_congr rfl fun i hi ↦ mul_rpow .. - _ ≤ (∑ i ∈ s, f i ^ p) ^ (r / p) * (∑ i ∈ s, g i ^ q) ^ (r / q) := by - apply inner_le_Lp_mul_Lq s _ _ this |>.trans_eq - congr! 2 - all_goals try simp only [fieldEq] - all_goals - refine s.sum_congr rfl fun i hi ↦ by simp [← rpow_mul, ← mul_div_assoc, hr.ne'] - -/-- **Hölder inequality**: The `L^r` norm of two functions is bounded by the -product of their `L^p` and `L^q` norms when `p`, `q`, and `r` form a `Real.HolderTriple`. -/ + have := hpqr.holderConjugate_div_div + calc ∑ i ∈ s, (f i * g i) ^ r + _ = ∑ i ∈ s, (f i) ^ r * (g i) ^ r := s.sum_congr rfl fun i hi ↦ mul_rpow .. + _ ≤ (∑ i ∈ s, f i ^ p) ^ (r / p) * (∑ i ∈ s, g i ^ q) ^ (r / q) := by + apply inner_le_Lp_mul_Lq s _ _ this |>.trans_eq + congr! 2 + all_goals try simp only [fieldEq] + all_goals + refine s.sum_congr rfl fun i hi ↦ by simp [← rpow_mul, ← mul_div_assoc, hpqr.pos'.ne'] + +/-- **Hölder inequality**: The `L^r` norm of the product of two functions is bounded by the +product of their `L^p` and `L^q` norms when `p`, `q`, and `r` form a `Real.HolderTriple`. -/ theorem Lr_le_Lp_mul_Lq (f g : ι → ℝ≥0) {p q r : ℝ} (hpqr : p.HolderTriple q r) : (∑ i ∈ s, (f i * g i) ^ r) ^ (1 / r) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q) := by @@ -549,10 +546,10 @@ lemma inner_le_weight_mul_Lp (s : Finset ι) {p : ℝ} (hp : 1 ≤ p) (w f : ι have hp₁ : 1 - p⁻¹ ≠ 0 := by simp [sub_eq_zero, hp.ne'] simp [mul_rpow, div_inv_eq_mul, one_mul, one_div, hp₀, hp₁] -/-- **Hölder inequality**: The (`r`-power of the) `L^r` norm of two functions is bounded by the -product of (the `r`-powers of) their `L^p` and `L^q` norms when `p`, `q`, and `r` form a -`Real.HolderTriple`. A version for `NNReal`-valued functions. For an alternative version, -convenient if the infinite sums are already expressed as powers, see `inner_le_Lp_mul_Lq_hasSum`. -/ +/-- **Hölder inequality**: The (`r`-power of the) `L^r` norm of the product of two functions is +bounded by the product of (the `r`-powers of) their `L^p` and `L^q` norms when `p`, `q`, and `r` +form a `Real.HolderTriple`. A version for `NNReal`-valued functions. For an alternative version, +convenient if the infinite sums are already expressed as powers, see `inner_le_Lp_mul_Lq_hasSum`. -/ theorem summable_and_Lr_rpow_le_Lp_mul_Lq_tsum {f g : ι → ℝ≥0} {p q r : ℝ} (hpqr : p.HolderTriple q r) (hf : Summable fun i => f i ^ p) (hg : Summable fun i => g i ^ q) : (Summable fun i => (f i * g i) ^ r) ∧ @@ -875,13 +872,13 @@ theorem Lr_le_Lp_mul_Lq_tsum_of_nonneg (hpqr : p.HolderTriple q r) (hf : ∀ i, -- It's really inconvenient that `positivity` can't use `∀` hypotheses. have hf' : 0 ≤ ∑' i, f i ^ p := tsum_nonneg fun i ↦ rpow_nonneg (hf i) p have hg' : 0 ≤ ∑' i, g i ^ q := tsum_nonneg fun i ↦ rpow_nonneg (hg i) q - obtain ⟨hp, hq, hr⟩ := hpqr.all_pos - convert rpow_le_rpow_iff (tsum_nonneg fun i ↦ rpow_nonneg (mul_nonneg (hf i) (hg i)) r) - (by apply mul_nonneg; all_goals apply rpow_nonneg; assumption) - (inv_eq_one_div r ▸ inv_pos.mpr hpqr.pos') |>.mpr <| - Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg hpqr hf hg hf_sum hg_sum using 1 - rw [mul_rpow (rpow_nonneg hf' _) (rpow_nonneg hg' _), ← Real.rpow_mul hg', ← Real.rpow_mul hf'] - field_simp + have hr := hpqr.pos' + convert rpow_le_rpow_iff (tsum_nonneg fun i ↦ rpow_nonneg (mul_nonneg (hf i) (hg i)) r) + (by apply mul_nonneg; all_goals apply rpow_nonneg; assumption) + (inv_eq_one_div r ▸ inv_pos.mpr hr) |>.mpr <| + Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg hpqr hf hg hf_sum hg_sum using 1 + rw [mul_rpow (rpow_nonneg hf' _) (rpow_nonneg hg' _), ← Real.rpow_mul hg', ← Real.rpow_mul hf'] + field_simp theorem inner_le_Lp_mul_Lq_tsum_of_nonneg (hpq : p.HolderConjugate q) (hf : ∀ i, 0 ≤ f i) (hg : ∀ i, 0 ≤ g i) (hf_sum : Summable fun i => f i ^ p) (hg_sum : Summable fun i => g i ^ q) : From 3586b7dcf4ff279c1ec118bcb1af23b89affef48 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Wed, 18 Mar 2026 12:38:37 -0500 Subject: [PATCH 3/3] fix line ending --- Mathlib/Analysis/MeanInequalities.lean | 52 +++++++++++++------------- 1 file changed, 26 insertions(+), 26 deletions(-) diff --git a/Mathlib/Analysis/MeanInequalities.lean b/Mathlib/Analysis/MeanInequalities.lean index 43e69c2353ca03..8fe04d53fd0bb9 100644 --- a/Mathlib/Analysis/MeanInequalities.lean +++ b/Mathlib/Analysis/MeanInequalities.lean @@ -502,23 +502,23 @@ theorem inner_le_Lp_mul_Lq (f g : ι → ℝ≥0) {p q : ℝ} (hpq : p.HolderCon · simp_rw [g', div_rpow, ← sum_div, ← rpow_mul, one_div, inv_mul_cancel₀ hpq.symm.ne_zero, rpow_one, div_self hg.ne'] -/-- **Hölder inequality**: The (`r`-power of the) `L^r` norm of the product of two functions is -bounded by the product of (the `r`-powers of) their `L^p` and `L^q` norms when `p`, `q`, and `r` -form a `Real.HolderTriple`. -/ +/-- **Hölder inequality**: The (`r`-power of the) `L^r` norm of the product of two functions is +bounded by the product of (the `r`-powers of) their `L^p` and `L^q` norms when `p`, `q`, and `r` +form a `Real.HolderTriple`. -/ theorem Lr_rpow_le_Lp_mul_Lq (f g : ι → ℝ≥0) {p q r : ℝ} (hpqr : p.HolderTriple q r) : ∑ i ∈ s, (f i * g i) ^ r ≤ (∑ i ∈ s, f i ^ p) ^ (r / p) * (∑ i ∈ s, g i ^ q) ^ (r / q) := by - have := hpqr.holderConjugate_div_div - calc ∑ i ∈ s, (f i * g i) ^ r - _ = ∑ i ∈ s, (f i) ^ r * (g i) ^ r := s.sum_congr rfl fun i hi ↦ mul_rpow .. - _ ≤ (∑ i ∈ s, f i ^ p) ^ (r / p) * (∑ i ∈ s, g i ^ q) ^ (r / q) := by - apply inner_le_Lp_mul_Lq s _ _ this |>.trans_eq - congr! 2 - all_goals try simp only [fieldEq] - all_goals - refine s.sum_congr rfl fun i hi ↦ by simp [← rpow_mul, ← mul_div_assoc, hpqr.pos'.ne'] - -/-- **Hölder inequality**: The `L^r` norm of the product of two functions is bounded by the -product of their `L^p` and `L^q` norms when `p`, `q`, and `r` form a `Real.HolderTriple`. -/ + have := hpqr.holderConjugate_div_div + calc ∑ i ∈ s, (f i * g i) ^ r + _ = ∑ i ∈ s, (f i) ^ r * (g i) ^ r := s.sum_congr rfl fun i hi ↦ mul_rpow .. + _ ≤ (∑ i ∈ s, f i ^ p) ^ (r / p) * (∑ i ∈ s, g i ^ q) ^ (r / q) := by + apply inner_le_Lp_mul_Lq s _ _ this |>.trans_eq + congr! 2 + all_goals try simp only [fieldEq] + all_goals + refine s.sum_congr rfl fun i hi ↦ by simp [← rpow_mul, ← mul_div_assoc, hpqr.pos'.ne'] + +/-- **Hölder inequality**: The `L^r` norm of the product of two functions is bounded by the +product of their `L^p` and `L^q` norms when `p`, `q`, and `r` form a `Real.HolderTriple`. -/ theorem Lr_le_Lp_mul_Lq (f g : ι → ℝ≥0) {p q r : ℝ} (hpqr : p.HolderTriple q r) : (∑ i ∈ s, (f i * g i) ^ r) ^ (1 / r) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q) := by @@ -546,10 +546,10 @@ lemma inner_le_weight_mul_Lp (s : Finset ι) {p : ℝ} (hp : 1 ≤ p) (w f : ι have hp₁ : 1 - p⁻¹ ≠ 0 := by simp [sub_eq_zero, hp.ne'] simp [mul_rpow, div_inv_eq_mul, one_mul, one_div, hp₀, hp₁] -/-- **Hölder inequality**: The (`r`-power of the) `L^r` norm of the product of two functions is -bounded by the product of (the `r`-powers of) their `L^p` and `L^q` norms when `p`, `q`, and `r` -form a `Real.HolderTriple`. A version for `NNReal`-valued functions. For an alternative version, -convenient if the infinite sums are already expressed as powers, see `inner_le_Lp_mul_Lq_hasSum`. -/ +/-- **Hölder inequality**: The (`r`-power of the) `L^r` norm of the product of two functions is +bounded by the product of (the `r`-powers of) their `L^p` and `L^q` norms when `p`, `q`, and `r` +form a `Real.HolderTriple`. A version for `NNReal`-valued functions. For an alternative version, +convenient if the infinite sums are already expressed as powers, see `inner_le_Lp_mul_Lq_hasSum`. -/ theorem summable_and_Lr_rpow_le_Lp_mul_Lq_tsum {f g : ι → ℝ≥0} {p q r : ℝ} (hpqr : p.HolderTriple q r) (hf : Summable fun i => f i ^ p) (hg : Summable fun i => g i ^ q) : (Summable fun i => (f i * g i) ^ r) ∧ @@ -872,13 +872,13 @@ theorem Lr_le_Lp_mul_Lq_tsum_of_nonneg (hpqr : p.HolderTriple q r) (hf : ∀ i, -- It's really inconvenient that `positivity` can't use `∀` hypotheses. have hf' : 0 ≤ ∑' i, f i ^ p := tsum_nonneg fun i ↦ rpow_nonneg (hf i) p have hg' : 0 ≤ ∑' i, g i ^ q := tsum_nonneg fun i ↦ rpow_nonneg (hg i) q - have hr := hpqr.pos' - convert rpow_le_rpow_iff (tsum_nonneg fun i ↦ rpow_nonneg (mul_nonneg (hf i) (hg i)) r) - (by apply mul_nonneg; all_goals apply rpow_nonneg; assumption) - (inv_eq_one_div r ▸ inv_pos.mpr hr) |>.mpr <| - Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg hpqr hf hg hf_sum hg_sum using 1 - rw [mul_rpow (rpow_nonneg hf' _) (rpow_nonneg hg' _), ← Real.rpow_mul hg', ← Real.rpow_mul hf'] - field_simp + have hr := hpqr.pos' + convert rpow_le_rpow_iff (tsum_nonneg fun i ↦ rpow_nonneg (mul_nonneg (hf i) (hg i)) r) + (by apply mul_nonneg; all_goals apply rpow_nonneg; assumption) + (inv_eq_one_div r ▸ inv_pos.mpr hr) |>.mpr <| + Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg hpqr hf hg hf_sum hg_sum using 1 + rw [mul_rpow (rpow_nonneg hf' _) (rpow_nonneg hg' _), ← Real.rpow_mul hg', ← Real.rpow_mul hf'] + field_simp theorem inner_le_Lp_mul_Lq_tsum_of_nonneg (hpq : p.HolderConjugate q) (hf : ∀ i, 0 ≤ f i) (hg : ∀ i, 0 ≤ g i) (hf_sum : Summable fun i => f i ^ p) (hg_sum : Summable fun i => g i ^ q) :