From a0bdae82a2001f65b6a514df93c301c5de4fb3e7 Mon Sep 17 00:00:00 2001 From: Evgenia Karunus Date: Tue, 7 Jul 2026 22:55:41 +0200 Subject: [PATCH 01/11] Convolution.lean - upsteramed `theorem convolution_symm` --- Mathlib/Analysis/Convolution.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Mathlib/Analysis/Convolution.lean b/Mathlib/Analysis/Convolution.lean index 2f7b10b145e3f6..76e7eed2d75793 100644 --- a/Mathlib/Analysis/Convolution.lean +++ b/Mathlib/Analysis/Convolution.lean @@ -645,6 +645,13 @@ theorem convolution_flip : g ⋆[L.flip, μ] f = f ⋆[L, μ] g := by rw [← integral_sub_left_eq_self _ μ x] simp_rw [sub_sub_self, flip_apply] +/-- Special case of `convolution_flip` when `L` is symmetric. -/ +theorem convolution_symm (L : E →L[𝕜] E →L[𝕜] F) (hL : ∀ (x y : E), L x y = L y x) {μ : Measure G} + [μ.IsAddLeftInvariant] [μ.IsNegInvariant] : + f ⋆[L, μ] f' = f' ⋆[L, μ] f := by + suffices L.flip = L by rw [← convolution_flip, this] + aesop + /-- The symmetric definition of convolution. -/ theorem convolution_eq_swap : (f ⋆[L, μ] g) x = ∫ t, L (f (x - t)) (g t) ∂μ := by rw [← convolution_flip]; rfl From b5dcf9c0f6bef8bf07fdc97b6b2ee2dac5a29da9 Mon Sep 17 00:00:00 2001 From: Evgenia Karunus Date: Tue, 7 Jul 2026 23:13:36 +0200 Subject: [PATCH 02/11] Convolution.lean - upstreamed `theorem AEStronglyMeasurable.convolution` --- Mathlib/Analysis/Convolution.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Mathlib/Analysis/Convolution.lean b/Mathlib/Analysis/Convolution.lean index 76e7eed2d75793..c38bbda874d750 100644 --- a/Mathlib/Analysis/Convolution.lean +++ b/Mathlib/Analysis/Convolution.lean @@ -517,6 +517,14 @@ section variable [MeasurableAdd₂ G] [MeasurableNeg G] [SFinite μ] [IsAddRightInvariant μ] +/-- The convolution of two a.e. strongly measurable functions is a.e. strongly measurable. -/ +@[fun_prop] +theorem AEStronglyMeasurable.convolution (hf : AEStronglyMeasurable f μ) + (hg : AEStronglyMeasurable g μ) : AEStronglyMeasurable (f ⋆[L, μ] g) μ := by + suffices AEStronglyMeasurable (fun ⟨x, t⟩ ↦ g (x - t)) (μ.prod μ) from + (L.aestronglyMeasurable_comp₂ hf.comp_snd this).integral_prod_right' + exact hg.comp_quasiMeasurePreserving (quasiMeasurePreserving_sub_of_right_invariant μ μ) + theorem Integrable.integrable_convolution (hf : Integrable f μ) (hg : Integrable g μ) : Integrable (f ⋆[L, μ] g) μ := (hf.convolution_integrand L hg).integral_prod_left From 8424917b6517f66c76a7e7fb896134973495483c Mon Sep 17 00:00:00 2001 From: Evgenia Karunus Date: Fri, 10 Jul 2026 04:44:55 +0200 Subject: [PATCH 03/11] Convolution.lean - upstreamed `lemma lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm` --- Mathlib/Analysis/Convolution.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/Mathlib/Analysis/Convolution.lean b/Mathlib/Analysis/Convolution.lean index c38bbda874d750..34432ca5a79c9d 100644 --- a/Mathlib/Analysis/Convolution.lean +++ b/Mathlib/Analysis/Convolution.lean @@ -686,6 +686,18 @@ theorem convolution_neg_of_neg_eq (h1 : ∀ᵐ x ∂μ, f (-x) = f x) (h2 : ∀ rw [← integral_neg_eq_self] simp only [neg_neg, ← sub_eq_add_neg] +omit [NormedSpace ℝ F] in +lemma lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm + [MeasurableAdd₂ G] [SFinite μ] + {p q : ENNReal} (hpq : p.HolderConjugate q) + (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖) + (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (x₀ : G) : + ∫⁻ a, ‖L (f a) (g (x₀ - a))‖ₑ ∂μ ≤ eLpNorm f p μ * eLpNorm g q μ := by + rw [← eLpNorm_comp_measurePreserving (p := q) hg (μ.measurePreserving_sub_left x₀)] + simpa [eLpNorm, eLpNorm'] using eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm hf + (hg.comp_quasiMeasurePreserving (quasiMeasurePreserving_sub_left μ x₀)) (L ·) 1 + (by simpa using Filter.Eventually.of_forall (fun x ↦ hL x (x₀ - x))) (hpqr := hpq) + end Measurable variable [TopologicalSpace G] From 14fe85c469f7b129b4eb2d336e4903b5c625724f Mon Sep 17 00:00:00 2001 From: Evgenia Karunus Date: Fri, 10 Jul 2026 04:57:02 +0200 Subject: [PATCH 04/11] Convolutin.lean - upstreamed `theorem of_memLp_memLp` --- Mathlib/Analysis/Convolution.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/Mathlib/Analysis/Convolution.lean b/Mathlib/Analysis/Convolution.lean index 34432ca5a79c9d..7e0a1ddb90e854 100644 --- a/Mathlib/Analysis/Convolution.lean +++ b/Mathlib/Analysis/Convolution.lean @@ -698,6 +698,21 @@ lemma lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm (hg.comp_quasiMeasurePreserving (quasiMeasurePreserving_sub_left μ x₀)) (L ·) 1 (by simpa using Filter.Eventually.of_forall (fun x ↦ hL x (x₀ - x))) (hpqr := hpq) +omit [NormedSpace ℝ F] in +/-- If `MemLp f p μ` and `MemLp g q μ`, where `p` and `q` are Hölder conjugates, then the +convolution of `f` and `g` exists everywhere. -/ +theorem ConvolutionExists.of_memLp_memLp + [μ.IsAddRightInvariant] [MeasurableAdd₂ G] [SFinite μ] + {p q : ENNReal} (hpq : p.HolderConjugate q) + (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖) + (hfp : MemLp f p μ) (hgq : MemLp g q μ) : + ConvolutionExists f g L μ := by + refine fun x ↦ + ⟨hfp.aestronglyMeasurable.convolution_integrand_snd L hgq.aestronglyMeasurable x, ?_⟩ + apply lt_of_le_of_lt (lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm L hpq hL + hfp.aestronglyMeasurable hgq.aestronglyMeasurable x) + finiteness + end Measurable variable [TopologicalSpace G] From 2ac0316f256fbf2a87fc07e9884fc840f44c9db4 Mon Sep 17 00:00:00 2001 From: Evgenia Karunus Date: Fri, 10 Jul 2026 04:59:52 +0200 Subject: [PATCH 05/11] Convolutions.lean - upstreamed `theorem enorm_convolution_le_eLpNorm_mul_eLpNorm` --- Mathlib/Analysis/Convolution.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/Mathlib/Analysis/Convolution.lean b/Mathlib/Analysis/Convolution.lean index 7e0a1ddb90e854..e6ff1ed2190a92 100644 --- a/Mathlib/Analysis/Convolution.lean +++ b/Mathlib/Analysis/Convolution.lean @@ -713,6 +713,16 @@ theorem ConvolutionExists.of_memLp_memLp hfp.aestronglyMeasurable hgq.aestronglyMeasurable x) finiteness +/-- If `p` and `q` are Hölder conjugates, then the convolution of `f` and `g` is bounded everywhere +by `eLpNorm f p μ * eLpNorm g q μ`. -/ +theorem enorm_convolution_le_eLpNorm_mul_eLpNorm + [MeasurableAdd₂ G] [SFinite μ] {p q : ENNReal} (hpq : p.HolderConjugate q) + (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖) + (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (x₀ : G) : + ‖(f ⋆[L, μ] g) x₀‖ₑ ≤ eLpNorm f p μ * eLpNorm g q μ := + (enorm_integral_le_lintegral_enorm _).trans <| + lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm L hpq hL hf hg x₀ + end Measurable variable [TopologicalSpace G] From e50569f14d6d953dba7f786b4b7e6c8ff5c60a1f Mon Sep 17 00:00:00 2001 From: Evgenia Karunus Date: Fri, 10 Jul 2026 05:05:46 +0200 Subject: [PATCH 06/11] excessive vars --- Mathlib/Analysis/Convolution.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Analysis/Convolution.lean b/Mathlib/Analysis/Convolution.lean index e6ff1ed2190a92..30a392d6509d41 100644 --- a/Mathlib/Analysis/Convolution.lean +++ b/Mathlib/Analysis/Convolution.lean @@ -654,8 +654,7 @@ theorem convolution_flip : g ⋆[L.flip, μ] f = f ⋆[L, μ] g := by simp_rw [sub_sub_self, flip_apply] /-- Special case of `convolution_flip` when `L` is symmetric. -/ -theorem convolution_symm (L : E →L[𝕜] E →L[𝕜] F) (hL : ∀ (x y : E), L x y = L y x) {μ : Measure G} - [μ.IsAddLeftInvariant] [μ.IsNegInvariant] : +theorem convolution_symm (L : E →L[𝕜] E →L[𝕜] F) (hL : ∀ (x y : E), L x y = L y x) : f ⋆[L, μ] f' = f' ⋆[L, μ] f := by suffices L.flip = L by rw [← convolution_flip, this] aesop From 7202a607dd7528357615d9ae87b54cbdf4925949 Mon Sep 17 00:00:00 2001 From: Evgenia Karunus Date: Sat, 11 Jul 2026 02:29:46 +0200 Subject: [PATCH 07/11] Convolution.lean - remove TODOs that we've done --- Mathlib/Analysis/Convolution.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Mathlib/Analysis/Convolution.lean b/Mathlib/Analysis/Convolution.lean index 30a392d6509d41..f556a6d8b6cebe 100644 --- a/Mathlib/Analysis/Convolution.lean +++ b/Mathlib/Analysis/Convolution.lean @@ -73,13 +73,11 @@ The following notations are localized in the scope `Convolution`: ## To do -* Existence and (uniform) continuity of the convolution if +* Uniform continuity of the convolution if one of the maps is in `ℒ^p` and the other in `ℒ^q` with `1 / p + 1 / q = 1`. This might require a generalization of `MeasureTheory.MemLp.smul` where `smul` is generalized to a continuous bilinear map. (see e.g. [Fremlin, *Measure Theory* (volume 2)][fremlin_vol2], 255K) -* The convolution is an `AEStronglyMeasurable` function - (see e.g. [Fremlin, *Measure Theory* (volume 2)][fremlin_vol2], 255I). * Prove properties about the convolution if both functions are rapidly decreasing. * Use `@[to_additive]` everywhere (this likely requires changes in `to_additive`) -/ From 43f52e45ffe84b268daf2eb0251aae588ee0a1a8 Mon Sep 17 00:00:00 2001 From: Evgenia Karunus Date: Sat, 11 Jul 2026 04:09:33 +0200 Subject: [PATCH 08/11] fix sections --- Mathlib/Analysis/Convolution.lean | 79 ++++++++++++++++--------------- 1 file changed, 40 insertions(+), 39 deletions(-) diff --git a/Mathlib/Analysis/Convolution.lean b/Mathlib/Analysis/Convolution.lean index f556a6d8b6cebe..d8cf7d1da82916 100644 --- a/Mathlib/Analysis/Convolution.lean +++ b/Mathlib/Analysis/Convolution.lean @@ -511,7 +511,7 @@ theorem support_convolution_subset_swap : support (f ⋆[L, μ] g) ⊆ support g · rw [h, L.map_zero₂] · exact (h <| sub_add_cancel x t).elim -section +section IsAddRightInvariant variable [MeasurableAdd₂ G] [MeasurableNeg G] [SFinite μ] [IsAddRightInvariant μ] @@ -527,7 +527,45 @@ theorem Integrable.integrable_convolution (hf : Integrable f μ) (hg : Integrable g μ) : Integrable (f ⋆[L, μ] g) μ := (hf.convolution_integrand L hg).integral_prod_left -end +end IsAddRightInvariant + +section IsAddLeftInvariant + +variable [MeasurableAdd₂ G] [MeasurableNeg G] [SFinite μ] [IsNegInvariant μ] [IsAddLeftInvariant μ] + +omit [NormedSpace ℝ F] in +lemma lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm {p q : ENNReal} + (hpq : p.HolderConjugate q) (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖) + (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (x₀ : G) : + ∫⁻ a, ‖L (f a) (g (x₀ - a))‖ₑ ∂μ ≤ eLpNorm f p μ * eLpNorm g q μ := by + rw [← eLpNorm_comp_measurePreserving (p := q) hg (μ.measurePreserving_sub_left x₀)] + simpa [eLpNorm, eLpNorm'] using eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm hf + (hg.comp_quasiMeasurePreserving (quasiMeasurePreserving_sub_left μ x₀)) (L ·) 1 + (by simpa using Filter.Eventually.of_forall (fun x ↦ hL x (x₀ - x))) (hpqr := hpq) + +omit [NormedSpace ℝ F] in +/-- If `MemLp f p μ` and `MemLp g q μ`, where `p` and `q` are Hölder conjugates, then the +convolution of `f` and `g` exists everywhere. -/ +theorem ConvolutionExists.of_memLp_memLp [IsAddRightInvariant μ] {p q : ENNReal} + (hpq : p.HolderConjugate q) (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖) + (hfp : MemLp f p μ) (hgq : MemLp g q μ) : + ConvolutionExists f g L μ := by + refine fun x ↦ + ⟨hfp.aestronglyMeasurable.convolution_integrand_snd L hgq.aestronglyMeasurable x, ?_⟩ + apply lt_of_le_of_lt (lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm L hpq hL + hfp.aestronglyMeasurable hgq.aestronglyMeasurable x) + finiteness + +/-- If `p` and `q` are Hölder conjugates, then the convolution of `f` and `g` is bounded everywhere +by `eLpNorm f p μ * eLpNorm g q μ`. -/ +theorem enorm_convolution_le_eLpNorm_mul_eLpNorm {p q : ENNReal} (hpq : p.HolderConjugate q) + (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖) (hf : AEStronglyMeasurable f μ) + (hg : AEStronglyMeasurable g μ) (x₀ : G) : + ‖(f ⋆[L, μ] g) x₀‖ₑ ≤ eLpNorm f p μ * eLpNorm g q μ := + (enorm_integral_le_lintegral_enorm _).trans <| + lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm L hpq hL hf hg x₀ + +end IsAddLeftInvariant variable [TopologicalSpace G] variable [IsTopologicalAddGroup G] @@ -683,43 +721,6 @@ theorem convolution_neg_of_neg_eq (h1 : ∀ᵐ x ∂μ, f (-x) = f x) (h2 : ∀ rw [← integral_neg_eq_self] simp only [neg_neg, ← sub_eq_add_neg] -omit [NormedSpace ℝ F] in -lemma lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm - [MeasurableAdd₂ G] [SFinite μ] - {p q : ENNReal} (hpq : p.HolderConjugate q) - (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖) - (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (x₀ : G) : - ∫⁻ a, ‖L (f a) (g (x₀ - a))‖ₑ ∂μ ≤ eLpNorm f p μ * eLpNorm g q μ := by - rw [← eLpNorm_comp_measurePreserving (p := q) hg (μ.measurePreserving_sub_left x₀)] - simpa [eLpNorm, eLpNorm'] using eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm hf - (hg.comp_quasiMeasurePreserving (quasiMeasurePreserving_sub_left μ x₀)) (L ·) 1 - (by simpa using Filter.Eventually.of_forall (fun x ↦ hL x (x₀ - x))) (hpqr := hpq) - -omit [NormedSpace ℝ F] in -/-- If `MemLp f p μ` and `MemLp g q μ`, where `p` and `q` are Hölder conjugates, then the -convolution of `f` and `g` exists everywhere. -/ -theorem ConvolutionExists.of_memLp_memLp - [μ.IsAddRightInvariant] [MeasurableAdd₂ G] [SFinite μ] - {p q : ENNReal} (hpq : p.HolderConjugate q) - (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖) - (hfp : MemLp f p μ) (hgq : MemLp g q μ) : - ConvolutionExists f g L μ := by - refine fun x ↦ - ⟨hfp.aestronglyMeasurable.convolution_integrand_snd L hgq.aestronglyMeasurable x, ?_⟩ - apply lt_of_le_of_lt (lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm L hpq hL - hfp.aestronglyMeasurable hgq.aestronglyMeasurable x) - finiteness - -/-- If `p` and `q` are Hölder conjugates, then the convolution of `f` and `g` is bounded everywhere -by `eLpNorm f p μ * eLpNorm g q μ`. -/ -theorem enorm_convolution_le_eLpNorm_mul_eLpNorm - [MeasurableAdd₂ G] [SFinite μ] {p q : ENNReal} (hpq : p.HolderConjugate q) - (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖) - (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (x₀ : G) : - ‖(f ⋆[L, μ] g) x₀‖ₑ ≤ eLpNorm f p μ * eLpNorm g q μ := - (enorm_integral_le_lintegral_enorm _).trans <| - lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm L hpq hL hf hg x₀ - end Measurable variable [TopologicalSpace G] From 34cae80a46df214c6d9b94666635d09f18da15e1 Mon Sep 17 00:00:00 2001 From: Evgenia Karunus Date: Sat, 11 Jul 2026 04:35:34 +0200 Subject: [PATCH 09/11] Convolution.lean - return `protected` back --- Mathlib/Analysis/Convolution.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/Convolution.lean b/Mathlib/Analysis/Convolution.lean index d8cf7d1da82916..5ab5f54005f35f 100644 --- a/Mathlib/Analysis/Convolution.lean +++ b/Mathlib/Analysis/Convolution.lean @@ -517,7 +517,7 @@ variable [MeasurableAdd₂ G] [MeasurableNeg G] [SFinite μ] [IsAddRightInvarian /-- The convolution of two a.e. strongly measurable functions is a.e. strongly measurable. -/ @[fun_prop] -theorem AEStronglyMeasurable.convolution (hf : AEStronglyMeasurable f μ) +protected theorem AEStronglyMeasurable.convolution (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) : AEStronglyMeasurable (f ⋆[L, μ] g) μ := by suffices AEStronglyMeasurable (fun ⟨x, t⟩ ↦ g (x - t)) (μ.prod μ) from (L.aestronglyMeasurable_comp₂ hf.comp_snd this).integral_prod_right' From 0752508118b30e1891fd126988ce96893d5d6acb Mon Sep 17 00:00:00 2001 From: Evgenia Karunus Date: Sun, 12 Jul 2026 03:26:12 +0200 Subject: [PATCH 10/11] Convolution.lean - from `(p.HolderConjugate q)` to `[p.HolderConjugate q]` --- Mathlib/Analysis/Convolution.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/Analysis/Convolution.lean b/Mathlib/Analysis/Convolution.lean index 5ab5f54005f35f..b964fac3d1f0ea 100644 --- a/Mathlib/Analysis/Convolution.lean +++ b/Mathlib/Analysis/Convolution.lean @@ -535,7 +535,7 @@ variable [MeasurableAdd₂ G] [MeasurableNeg G] [SFinite μ] [IsNegInvariant μ] omit [NormedSpace ℝ F] in lemma lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm {p q : ENNReal} - (hpq : p.HolderConjugate q) (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖) + [hpq : p.HolderConjugate q] (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖) (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (x₀ : G) : ∫⁻ a, ‖L (f a) (g (x₀ - a))‖ₑ ∂μ ≤ eLpNorm f p μ * eLpNorm g q μ := by rw [← eLpNorm_comp_measurePreserving (p := q) hg (μ.measurePreserving_sub_left x₀)] @@ -547,23 +547,23 @@ omit [NormedSpace ℝ F] in /-- If `MemLp f p μ` and `MemLp g q μ`, where `p` and `q` are Hölder conjugates, then the convolution of `f` and `g` exists everywhere. -/ theorem ConvolutionExists.of_memLp_memLp [IsAddRightInvariant μ] {p q : ENNReal} - (hpq : p.HolderConjugate q) (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖) + [hpq : p.HolderConjugate q] (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖) (hfp : MemLp f p μ) (hgq : MemLp g q μ) : ConvolutionExists f g L μ := by refine fun x ↦ ⟨hfp.aestronglyMeasurable.convolution_integrand_snd L hgq.aestronglyMeasurable x, ?_⟩ - apply lt_of_le_of_lt (lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm L hpq hL - hfp.aestronglyMeasurable hgq.aestronglyMeasurable x) + apply lt_of_le_of_lt (lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm L hL + hfp.aestronglyMeasurable hgq.aestronglyMeasurable x (hpq := hpq)) finiteness /-- If `p` and `q` are Hölder conjugates, then the convolution of `f` and `g` is bounded everywhere by `eLpNorm f p μ * eLpNorm g q μ`. -/ -theorem enorm_convolution_le_eLpNorm_mul_eLpNorm {p q : ENNReal} (hpq : p.HolderConjugate q) +theorem enorm_convolution_le_eLpNorm_mul_eLpNorm {p q : ENNReal} [hpq : p.HolderConjugate q] (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖) (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (x₀ : G) : ‖(f ⋆[L, μ] g) x₀‖ₑ ≤ eLpNorm f p μ * eLpNorm g q μ := (enorm_integral_le_lintegral_enorm _).trans <| - lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm L hpq hL hf hg x₀ + lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm L hL hf hg x₀ end IsAddLeftInvariant From 2c77bfe2e27cd9e0aaabc2a44bb1ce267e1cbafc Mon Sep 17 00:00:00 2001 From: Evgenia Karunus Date: Sun, 12 Jul 2026 03:36:43 +0200 Subject: [PATCH 11/11] lemma lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm - refactor some more --- Mathlib/Analysis/Convolution.lean | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/Mathlib/Analysis/Convolution.lean b/Mathlib/Analysis/Convolution.lean index b964fac3d1f0ea..3063152b83ae14 100644 --- a/Mathlib/Analysis/Convolution.lean +++ b/Mathlib/Analysis/Convolution.lean @@ -538,10 +538,13 @@ lemma lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm {p q : ENNRea [hpq : p.HolderConjugate q] (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖) (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (x₀ : G) : ∫⁻ a, ‖L (f a) (g (x₀ - a))‖ₑ ∂μ ≤ eLpNorm f p μ * eLpNorm g q μ := by - rw [← eLpNorm_comp_measurePreserving (p := q) hg (μ.measurePreserving_sub_left x₀)] - simpa [eLpNorm, eLpNorm'] using eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm hf - (hg.comp_quasiMeasurePreserving (quasiMeasurePreserving_sub_left μ x₀)) (L ·) 1 - (by simpa using Filter.Eventually.of_forall (fun x ↦ hL x (x₀ - x))) (hpqr := hpq) + rw [← eLpNorm_comp_measurePreserving hg (μ.measurePreserving_sub_left x₀)] + have hg' : AEStronglyMeasurable (g ∘ fun h ↦ x₀ - h) μ := + (hg.comp_quasiMeasurePreserving (quasiMeasurePreserving_sub_left μ x₀)) + have hL' : ∀ᵐ (x : G) ∂μ, ‖L (f x) (g (x₀ - x))‖ ≤ (1 : NNReal) * ‖f x‖ * ‖g (x₀ - x)‖ := by + simpa using Eventually.of_forall (fun x ↦ hL x (x₀ - x)) + simpa [eLpNorm, eLpNorm'] + using eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm hf hg' (L ·) 1 hL' (hpqr := hpq) omit [NormedSpace ℝ F] in /-- If `MemLp f p μ` and `MemLp g q μ`, where `p` and `q` are Hölder conjugates, then the