Source indexedtheorem · leanprover/lean4:v4.32.0

ENNReal.eLpNorm_Ioc_convolution_le_of_norm_le_mul

Carleson.ToMathlib.MeasureTheory.Integral.MeanInequalities · Carleson/ToMathlib/MeasureTheory/Integral/MeanInequalities.lean:527 to 559

Source documentation

Young's convolution inequality on (a, a + T]: the L^r seminorm of the convolution of T-periodic functions over (a, a + T] is bounded by ‖L‖ₑ times the product of the L^p and L^q seminorms on that interval, where 1 / p + 1 / q = 1 / r + 1. Here ‖L‖ₑ is replaced with a bound for L restricted to the ranges of f and g; see eLpNorm_Ioc_convolution_le_enorm_mul for a version using ‖L‖ₑ explicitly.

Exact Lean statement

theorem eLpNorm_Ioc_convolution_le_of_norm_le_mul (a : ℝ) {T : ℝ} [hT : Fact (0 < T)]
    {p q r : ℝ≥0∞} (hp : 1 ≤ p) (hq : 1 ≤ q) (hr : 1 ≤ r) (hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1)
    {f : ℝ → E} {g : ℝ → E'} (hgT : g.Periodic T)
    (hf : AEStronglyMeasurable f) (hg : AEStronglyMeasurable g)
    (c : ℝ) (hL : ∀ (x y : ℝ), ‖L (f x) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖) :
    eLpNorm (fun x ↦ ∫ y in a..a+T, L (f y) (g (x - y))) r (volume.restrict (Ioc a (a + T))) ≤
    .ofReal c * eLpNorm f p (volume.restrict (Ioc a (a + T))) *
      eLpNorm g q (volume.restrict (Ioc a (a + T)))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem eLpNorm_Ioc_convolution_le_of_norm_le_mul (a : ℝ) {T : ℝ} [hT : Fact (0 < T)]    {p q r : ℝ≥0∞} (hp : 1 ≤ p) (hq : 1 ≤ q) (hr : 1 ≤ r) (hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1)    {f : ℝ → E} {g : ℝ → E'} (hgT : g.Periodic T)    (hf : AEStronglyMeasurable f) (hg : AEStronglyMeasurable g)    (c : ℝ) (hL : ∀ (x y : ℝ), ‖L (f x) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖) :    eLpNorm (fun x ↦ ∫ y in a..a+T, L (f y) (g (x - y))) r (volume.restrict (Ioc a (a + T))) ≤    .ofReal c * eLpNorm f p (volume.restrict (Ioc a (a + T))) *      eLpNorm g q (volume.restrict (Ioc a (a + T))) := by  let f' := AddCircle.liftIoc T a f  let f'' := fun (x : ℝ) ↦ f' x  have hfT : f''.Periodic T := by simp [Function.Periodic, f'']  have : eLpNorm (fun x ↦ ∫ y in a..a+T, L (f'' y) (g (x - y))) r        (volume.restrict (Ioc a (a + T))) ≤      .ofReal c * eLpNorm f'' p (volume.restrict (Ioc a (a + T))) *      eLpNorm g q (volume.restrict (Ioc a (a + T))) := by    apply eLpNorm_Ioc_convolution_le_of_norm_le_mul_aux L a hp hq hr hpqr hfT hgT _ hg    · intro x y      simp only [liftIoc, Function.comp_apply, restrict_apply, f'', f']      apply hL    have A : AEStronglyMeasurable f'        (Measure.map (fun (x : ℝ) ↦ (x : AddCircle T)) (volume : Measure ℝ)) :=      AEStronglyMeasurable.mono_ac (quasiMeasurePreserving_coe_addCircle T).absolutelyContinuous        (by fun_prop)    exact A.comp_measurable (by fun_prop)  convert this using 3 with x  · rw [intervalIntegral.integral_of_le (by linarith [hT.out]),      intervalIntegral.integral_of_le (by linarith [hT.out])]    apply setIntegral_congr_fun measurableSet_Ioc (fun y hy ↦ ?_)    congr 2    exact (AddCircle.liftIoc_coe_apply hy).symm  · apply eLpNorm_congr_ae    filter_upwards [self_mem_ae_restrict measurableSet_Ioc] with y hy    exact (AddCircle.liftIoc_coe_apply hy).symm