Source indexedlemma · leanprover/lean4:v4.32.0

eLpNorm_convolution_dirichletApprox

Carleson.Classical.HilbertStrongType · Carleson/Classical/HilbertStrongType.lean:459 to 484

Source documentation

The convolution with dirichletApprox is controlled on (0, 2π] in L^2 norm. This follows from the fact that it coincides (up to a constant) with approxHilbertTransform, which is essentially an average of Fourier projections (which are all contractions in L^2).

Exact Lean statement

lemma eLpNorm_convolution_dirichletApprox {g : ℝ → ℂ} {n : ℕ} (hg : MemLp g ∞ volume) :
    eLpNorm (fun x ↦ ∫ y in (0)..2 * π, g y * dirichletApprox n (x - y))
      2 (volume.restrict (Ioc 0 (2 * π))) ≤
    7 * eLpNorm g 2 (volume.restrict (Ioc 0 (2 * π)))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma eLpNorm_convolution_dirichletApprox {g : ℝ → ℂ} {n : ℕ} (hg : MemLp g ∞ volume) :    eLpNorm (fun x ↦ ∫ y in (0)..2 * π, g y * dirichletApprox n (x - y))      2 (volume.restrict (Ioc 0 (2 * π))) ≤    7 * eLpNorm g 2 (volume.restrict (Ioc 0 (2 * π))) := by  have : (fun x ↦ ∫ y in (0)..2 * π, g y * dirichletApprox n (x - y)) =      (2 * π) • fun x ↦ approxHilbertTransform n g x := by    ext x    simp only [Pi.smul_apply, real_smul, ofReal_mul, ofReal_ofNat, ofReal_inv,      approxHilbertTransform_eq_dirichletApprox hg, ← mul_assoc, Pi.smul_apply]    rw [mul_inv_cancel₀ (by simp [Real.pi_ne_zero]), one_mul]  rw [    this,    show    eLpNorm ((2 * π : ℝ) • fun x ↦ approxHilbertTransform n g x) 2 (volume.restrict (Ioc 0 (2 * π))) =    ‖(2 * π : ℝ)‖ₑ * eLpNorm (fun x ↦ approxHilbertTransform n g x) 2 (volume.restrict (Ioc 0 (2 * π)))    from eLpNorm_const_smul ..  ]  gcongr  · have A : ‖2 * π‖ₑ = ENNReal.ofReal (2 * π) := by      refine Real.enorm_of_nonneg ?_      simp [Real.pi_nonneg]    rw [A]    apply ENNReal.ofReal_le_of_le_toReal    simp only [ENNReal.toReal_ofNat]    linarith [Real.pi_lt_d2]  · apply modulated_averaged_projection' hg.aestronglyMeasurable.aemeasurable