Proof of Young's convolution inequality

Carleson.lean

@@ -37,14 +37,22 @@ import Carleson.MinLayerTiles
 import Carleson.Psi
 import Carleson.TileExistence
 import Carleson.TileStructure
+import Carleson.ToMathlib.Analysis.Convolution
 import Carleson.ToMathlib.Annulus
 import Carleson.ToMathlib.BoundedCompactSupport
 import Carleson.ToMathlib.CoverByBalls
+import Carleson.ToMathlib.Data.Real.ConjExponents
 import Carleson.ToMathlib.DoublingMeasure
 import Carleson.ToMathlib.ENorm
 import Carleson.ToMathlib.HardyLittlewood
 import Carleson.ToMathlib.MeasureReal
+import Carleson.ToMathlib.MeasureTheory.Function.LpSeminorm.Basic
+import Carleson.ToMathlib.MeasureTheory.Group.LIntegral
+import Carleson.ToMathlib.MeasureTheory.Integral.Lebesgue
+import Carleson.ToMathlib.MeasureTheory.Integral.MeanInequalities
 import Carleson.ToMathlib.MeasureTheory.Integral.SetIntegral
+import Carleson.ToMathlib.MeasureTheory.Measure.Haar.Unique
+import Carleson.ToMathlib.MeasureTheory.Measure.Prod
 import Carleson.ToMathlib.MinLayer
 import Carleson.ToMathlib.Misc
 import Carleson.ToMathlib.RealInterpolation

Carleson/ToMathlib/Analysis/Convolution.lean

@@ -0,0 +1,80 @@
+import Mathlib.Analysis.Convolution
+
+open scoped Convolution
+
+namespace MeasureTheory
+
+universe u𝕜 uG uE uE' uF
+
+variable {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF}
+
+variable [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F]
+  {f : G → E} {g : G → E'}
+
+variable [NontriviallyNormedField 𝕜]
+
+variable [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F]
+variable {L : E →L[𝕜] E' →L[𝕜] F}
+
+variable [MeasurableSpace G]
+
+/-- Special case of ``convolution_flip` when `L` is symmetric. -/
+theorem convolution_symm {f : G → E} {g : G → E} (L : E →L[𝕜] E →L[𝕜] F)
+    (hL : ∀ (x y : E), L x y = L y x) [NormedSpace ℝ F] [AddCommGroup G]
+    {μ : Measure G} [μ.IsAddLeftInvariant] [μ.IsNegInvariant] [MeasurableNeg G] [MeasurableAdd G] :
+    f ⋆[L, μ] g = g ⋆[L, μ] f := by
+  suffices L.flip = L by rw [← convolution_flip, this]
+  ext x y
+  exact hL y x
+
+/-- The convolution of two a.e. strongly measurable functions is a.e. strongly measurable. -/
+theorem aestronglyMeasurable_convolution [NormedSpace ℝ F] [AddGroup G] [MeasurableAdd₂ G]
+    [MeasurableNeg G] {μ : Measure G} [SigmaFinite μ] [μ.IsAddRightInvariant]
+    (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.snd this).integral_prod_right'
+  refine hg.comp_quasiMeasurePreserving <| QuasiMeasurePreserving.prod_of_left measurable_sub ?_
+  apply Filter.Eventually.of_forall (fun x ↦ ?_)
+  exact ⟨measurable_sub_const x, by rw [map_sub_right_eq_self μ x]⟩
+
+/-- This implies both of the following theorems `convolutionExists_of_memℒp_memℒp` and
+`enorm_convolution_le_eLpNorm_mul_eLpNorm`. -/
+lemma lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm [NormedSpace ℝ F] [AddGroup G]
+    [MeasurableAdd₂ G] [MeasurableNeg G] {μ : Measure G} [SFinite μ] [μ.IsNegInvariant]
+    [μ.IsAddLeftInvariant] {p q : ENNReal} (hpq : p.IsConjExponent q)
+    (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖)
+    (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (x₀ : G) :
+    ∫⁻ (a : G), ‖(L (f a)) (g (x₀ - a))‖ₑ ∂μ ≤ eLpNorm f p μ * eLpNorm g q μ := by
+  rw [eLpNorm_comp_measurePreserving (p := q) hg (μ.measurePreserving_sub_left x₀) |>.symm]
+  replace hpq : 1 / 1 = 1 / p + 1 /q := by simpa using hpq.inv_add_inv_conj.symm
+  have hg' : AEStronglyMeasurable (g <| x₀ - ·) μ :=
+    hg.comp_quasiMeasurePreserving <| quasiMeasurePreserving_sub_left μ x₀
+  have hL' : ∀ᵐ (x : G) ∂μ, ‖L (f x) (g (x₀ - x))‖ ≤ ‖f x‖ * ‖g (x₀ - x)‖ :=
+    Filter.Eventually.of_forall (fun x ↦ hL x (x₀ - x))
+  simpa [eLpNorm, eLpNorm'] using eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm hf hg' (L ·) hL' hpq
+
+/-- If `Memℒp f p μ` and `Memℒp g q μ`, where `p` and `q` are Hölder conjugates, then the
+convolution of `f` and `g` exists everywhere. -/
+theorem convolutionExists_of_memℒp_memℒp [NormedSpace ℝ F] [AddGroup G] [MeasurableAdd₂ G]
+    [MeasurableNeg G] (μ : Measure G) [SFinite μ] [μ.IsNegInvariant] [μ.IsAddLeftInvariant]
+    [μ.IsAddRightInvariant] {p q : ENNReal} (hpq : p.IsConjExponent q)
+    (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖) (hf : AEStronglyMeasurable f μ)
+    (hg : AEStronglyMeasurable g μ) (hfp : Memℒp f p μ) (hgq : Memℒp g q μ) :
+    ConvolutionExists f g L μ := by
+  refine fun x ↦ ⟨AEStronglyMeasurable.convolution_integrand_snd L hf hg x, ?_⟩
+  apply lt_of_le_of_lt (lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm hpq hL hf hg x)
+  exact ENNReal.mul_lt_top hfp.eLpNorm_lt_top hgq.eLpNorm_lt_top
+
+/-- 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 [NormedSpace ℝ F] [AddGroup G]
+    [MeasurableAdd₂ G] [MeasurableNeg G] (μ : Measure G) [SFinite μ] [μ.IsNegInvariant]
+    [μ.IsAddLeftInvariant] [μ.IsAddRightInvariant] {p q : ENNReal} (hpq : p.IsConjExponent 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 hpq hL hf hg x₀
+
+end MeasureTheory

Carleson/ToMathlib/Data/Real/ConjExponents.lean

@@ -0,0 +1,23 @@
+import Mathlib.Data.Real.ConjExponents
+
+open scoped ENNReal
+
+namespace ENNReal
+namespace IsConjExponent
+
+variable {p q : ℝ≥0∞} (h : p.IsConjExponent q)
+
+section
+include h
+
+lemma conjExponent_toReal (hp : p ≠ ∞) (hq : q ≠ ∞) : p.toReal.IsConjExponent q.toReal := by
+  constructor
+  · rw [← ENNReal.ofReal_lt_iff_lt_toReal one_pos.le hp, ofReal_one]
+    exact h.one_le.lt_of_ne (fun p_eq_1 ↦ hq (by simpa [p_eq_1] using h.conj_eq))
+  · rw [← toReal_inv, ← toReal_inv, ← toReal_add, h.inv_add_inv_conj, ENNReal.toReal_eq_one_iff]
+    · exact ENNReal.inv_ne_top.mpr h.ne_zero
+    · exact ENNReal.inv_ne_top.mpr h.symm.ne_zero
+
+end
+end IsConjExponent
+end ENNReal

Carleson/ToMathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

@@ -0,0 +1,41 @@
+import Mathlib.MeasureTheory.Function.LpSeminorm.Basic
+import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
+import Mathlib.Analysis.Normed.Group.Basic
+
+open MeasureTheory
+open scoped ENNReal
+
+variable {α ε E F G : Type*} {m m0 : MeasurableSpace α} {p : ℝ≥0∞} {q : ℝ} {μ ν : Measure α}
+  [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [ENorm ε]
+
+namespace MeasureTheory
+
+section MapMeasure
+
+variable {β : Type*} {mβ : MeasurableSpace β} {f : α → β} {g : β → E}
+
+theorem eLpNormEssSup_map_measure' [MeasurableSpace E] [OpensMeasurableSpace E]
+    (hg : AEMeasurable g (Measure.map f μ)) (hf : AEMeasurable f μ) :
+    eLpNormEssSup g (Measure.map f μ) = eLpNormEssSup (g ∘ f) μ :=
+  essSup_map_measure hg.enorm hf
+
+theorem eLpNorm_map_measure' [MeasurableSpace E] [OpensMeasurableSpace E]
+    (hg : AEMeasurable g (Measure.map f μ)) (hf : AEMeasurable f μ) :
+    eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ := by
+  by_cases hp_zero : p = 0
+  · simp only [hp_zero, eLpNorm_exponent_zero]
+  by_cases hp_top : p = ∞
+  · simp_rw [hp_top, eLpNorm_exponent_top]
+    exact eLpNormEssSup_map_measure' hg hf
+  simp_rw [eLpNorm_eq_lintegral_rpow_enorm hp_zero hp_top]
+  rw [lintegral_map' (hg.enorm.pow_const p.toReal) hf]
+  rfl
+
+theorem eLpNorm_comp_measurePreserving' {ν : MeasureTheory.Measure β} [MeasurableSpace E]
+    [OpensMeasurableSpace E] (hg : AEMeasurable g ν) (hf : MeasurePreserving f μ ν) :
+    eLpNorm (g ∘ f) p μ = eLpNorm g p ν :=
+  Eq.symm <| hf.map_eq ▸ eLpNorm_map_measure' (hf.map_eq ▸ hg) hf.aemeasurable
+
+end MapMeasure
+
+end MeasureTheory

Carleson/ToMathlib/MeasureTheory/Group/LIntegral.lean

@@ -0,0 +1,34 @@
+import Mathlib.MeasureTheory.Group.LIntegral
+
+namespace MeasureTheory
+
+open Measure
+open scoped ENNReal
+
+variable {G : Type*} [MeasurableSpace G] {μ : Measure G}
+
+section MeasurableInv
+variable [Group G] [MeasurableInv G]
+
+/-- If `μ` is invariant under inversion, then `∫⁻ x, f x ∂μ` is unchanged by replacing
+`x` with `x⁻¹` -/
+@[to_additive
+  "If `μ` is invariant under negation, then `∫⁻ x, f x ∂μ` is unchanged by replacing `x` with `-x`"]
+theorem lintegral_inv_eq_self [μ.IsInvInvariant] (f : G → ℝ≥0∞) :
+    ∫⁻ (x : G), f x⁻¹ ∂μ = ∫⁻ (x : G), f x ∂μ := by
+  simpa using (lintegral_map_equiv f (μ := μ) <| MeasurableEquiv.inv G).symm
+
+end MeasurableInv
+
+section MeasurableMul
+
+variable [Group G] [MeasurableMul G]
+
+@[to_additive]
+theorem lintegral_div_left_eq_self [IsMulLeftInvariant μ] [MeasurableInv G] [IsInvInvariant μ]
+    (f : G → ℝ≥0∞) (g : G) : (∫⁻ x, f (g / x) ∂μ) = ∫⁻ x, f x ∂μ := by
+  simp_rw [div_eq_mul_inv, lintegral_inv_eq_self (f <| g * ·), lintegral_mul_left_eq_self]
+
+end MeasurableMul
+
+end MeasureTheory

Carleson/ToMathlib/MeasureTheory/Integral/Lebesgue.lean

@@ -0,0 +1,33 @@
+import Mathlib.MeasureTheory.Integral.Lebesgue
+
+open ENNReal
+
+namespace MeasureTheory
+
+open SimpleFunc
+
+/-- Generalization of `MeasureTheory.lintegral_eq_iSup_eapprox_lintegral` assuming a.e.
+measurability of `f` -/
+theorem lintegral_eq_iSup_eapprox_lintegral' {α : Type*} {m : MeasurableSpace α} {μ : Measure α}
+    {f : α → ENNReal} (hf : AEMeasurable f μ) :
+    ∫⁻ (a : α), f a ∂μ = ⨆ (n : ℕ), (eapprox (hf.mk f) n).lintegral μ := calc
+  _ = ∫⁻ a, hf.mk f a ∂μ                                    := lintegral_congr_ae hf.ae_eq_mk
+  _ = ∫⁻ a, ⨆ n, (eapprox (hf.mk f) n : α → ℝ≥0∞) a ∂μ      := by
+    congr; ext a; rw [iSup_eapprox_apply hf.measurable_mk]
+  _ = ⨆ n, ∫⁻ a, eapprox (hf.mk f) n a ∂μ                   :=
+    lintegral_iSup (fun _ ↦ SimpleFunc.measurable _) (fun _ _ h ↦ monotone_eapprox (hf.mk f) h)
+  _ = ⨆ n, (eapprox (hf.mk f) n).lintegral μ                := by simp_rw [lintegral_eq_lintegral]
+
+/-- Generalization of `MeasureTheory.lintegral_comp` assuming a.e. measurability of `f` and `g` -/
+theorem lintegral_comp' {α : Type*} {β : Type*} {m : MeasurableSpace α} {μ : Measure α}
+    [MeasurableSpace β] {f : β → ENNReal} {g : α → β} (hf : AEMeasurable f (μ.map g))
+    (hg : AEMeasurable g μ) : lintegral μ (f ∘ g) = ∫⁻ a, f a ∂μ.map g := by
+  rw [μ.map_congr hg.ae_eq_mk] at hf ⊢
+  calc  ∫⁻ a, (f ∘ g) a ∂μ
+    _ = ∫⁻ a, (hf.mk f ∘ hg.mk g) a ∂μ     := by
+      rw [lintegral_congr_ae (hg.ae_eq_mk.fun_comp f)]
+      exact lintegral_congr_ae (ae_of_ae_map hg.measurable_mk.aemeasurable hf.ae_eq_mk)
+    _ = ∫⁻ a, hf.mk f a ∂μ.map (hg.mk g)   := lintegral_comp hf.measurable_mk hg.measurable_mk
+    _ = ∫⁻ a, f a ∂μ.map (hg.mk g)         := lintegral_congr_ae hf.ae_eq_mk.symm
+
+end MeasureTheory