Source indexedlemma · leanprover/lean4:v4.32.0

young_convolution

Carleson.Classical.HilbertStrongType · Carleson/Classical/HilbertStrongType.lean:291 to 299

Source documentation

Lemma 11.3.3.

Exact Lean statement

lemma young_convolution {f g : ℝ → ℝ} (hmf : AEMeasurable f)
    (hmg : AEMeasurable g) (periodic_g : g.Periodic (2 * π)) :
    eLpNorm (fun x ↦ ∫ y in (0)..2 * π, f y * g (x - y)) 2 (volume.restrict (Ioc 0 (2 * π))) ≤
      eLpNorm f 2 (volume.restrict (Ioc 0 (2 * π)))
      * eLpNorm g 1 (volume.restrict (Ioc 0 (2 * π)))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma young_convolution {f g : ℝ → ℝ} (hmf : AEMeasurable f)    (hmg : AEMeasurable g) (periodic_g : g.Periodic (2 * π)) :    eLpNorm (fun x ↦ ∫ y in (0)..2 * π, f y * g (x - y)) 2 (volume.restrict (Ioc 0 (2 * π))) ≤      eLpNorm f 2 (volume.restrict (Ioc 0 (2 * π)))      * eLpNorm g 1 (volume.restrict (Ioc 0 (2 * π))) := by  have h2 : (1 : ℝ≥0∞) ≤ 2 := by exact one_le_two  simpa [zero_add] using ENNReal.eLpNorm_Ioc_convolution_le_of_norm_le_mul    (ContinuousLinearMap.mul ℝ ℝ) 0 h2 (le_refl 1) h2 (by rw [inv_one])    periodic_g hmf.aestronglyMeasurable hmg.aestronglyMeasurable 1 (by simp)