Source indexedlemma · leanprover/lean4:v4.32.0

eLpNorm_czOperator_restrict_two_three_of_support_subset

Carleson.Classical.HilbertStrongType · Carleson/Classical/HilbertStrongType.lean:769 to 840

Source documentation

The operator czOperator K r is bounded from L^2 ([1, 4]) to L^2 ([2, 3]), uniformly in r. This follows from the fact, proved in norm_czOperator_le_add, that it is bounded by the sum of two operators which are both bounded: one is the convolution with dirichletApprox, bounded as it is an average of Fourier projections, and the other one has a kernel uniformly bounded in L^1 and is therefore controlled by Young inequality.

In this version, we assume that the function is supported in [1, 4], but we will drop this assumption just after this lemma, in eLpNorm_czOperator_restrict_two_three.

Exact Lean statement

lemma eLpNorm_czOperator_restrict_two_three_of_support_subset {g : ℝ → ℂ} {r : ℝ}
    (hr : r ∈ Ioo 0 1) (hg : MemLp g ∞ volume) (h'g : support g ⊆ Icc 1 4) :
    eLpNorm (czOperator K r g) 2 (volume.restrict (Ioc 2 3)) ≤
      2 ^ 8 * eLpNorm g 2 (volume.restrict (Ioc 1 4))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma eLpNorm_czOperator_restrict_two_three_of_support_subset {g : ℝ → ℂ} {r : ℝ}    (hr : r ∈ Ioo 0 1) (hg : MemLp g ∞ volume) (h'g : support g ⊆ Icc 1 4) :    eLpNorm (czOperator K r g) 2 (volume.restrict (Ioc 2 3)) ≤      2 ^ 8 * eLpNorm g 2 (volume.restrict (Ioc 1 4)) := by  have I : 0 ≤ 2 * π := by linarith [Real.pi_nonneg]  set n := ⌈r⁻¹⌉₊ with hn  calc  eLpNorm (czOperator K r g) 2 (volume.restrict (Ioc 2 3))  _ ≤ eLpNorm (fun x ↦ ‖∫ y in (0)..(2 * π), g y * dirichletApprox n (x - y)‖      + 12 * ∫ y in Ioc 0 (2 * π), ‖g y‖ * niceKernel r (x - y)) 2 (volume.restrict (Ioc 2 3)) := by    apply eLpNorm_mono_ae_real    filter_upwards [self_mem_ae_restrict measurableSet_Ioc] with x hx    apply norm_czOperator_le_add hr  hn hg hx.1.le hx.2 h'g  _ ≤ eLpNorm (fun x ↦ ‖∫ y in (0)..(2 * π), g y * dirichletApprox n (x - y)‖      + 12 * ∫ y in Ioc 0 (2 * π), ‖g y‖ * niceKernel r (x - y)) 2      (volume.restrict (Ioc 0 (2 * π))) := by    apply eLpNorm_mono_measure    apply Measure.restrict_mono _ le_rfl    apply Ioc_subset_Ioc (by norm_num)    linarith [Real.pi_gt_three]  _ ≤ eLpNorm (fun x ↦ ‖∫ y in (0)..(2 * π), g y * dirichletApprox n (x - y)‖) 2      (volume.restrict (Ioc 0 (2 * π)))     + eLpNorm (fun x ↦ 12 * ∫ y in Ioc 0 (2 * π), ‖g y‖ * niceKernel r (x - y)) 2      (volume.restrict (Ioc 0 (2 * π))) := by    apply eLpNorm_add_le _ _ one_le_two    · apply AEStronglyMeasurable.norm      simp_rw [intervalIntegral.integral_of_le I]      let L := ContinuousLinearMap.mul ℂ ℂ      let w : ℝ × ℝ → ℂ := fun p ↦ L (g p.2) (dirichletApprox n (p.1 - p.2))      change AEStronglyMeasurable (fun x ↦ ∫ (y : ℝ) in Ioc 0 (2 * π), w (x, y) ∂volume)        (volume.restrict (Ioc 0 (2 * π)))      apply AEStronglyMeasurable.integral_prod_right'      apply (hg.restrict _).aestronglyMeasurable.convolution_integrand'      fun_prop    · apply AEStronglyMeasurable.const_mul      let L := ContinuousLinearMap.mul ℝ ℝ      let w : ℝ × ℝ → ℝ := fun p ↦ L (‖g p.2‖) (niceKernel r (p.1 - p.2))      change AEStronglyMeasurable (fun x ↦ ∫ (y : ℝ) in Ioc 0 (2 * π), w (x, y) ∂volume)        (volume.restrict (Ioc 0 (2 * π)))      apply AEStronglyMeasurable.integral_prod_right'      apply (hg.norm.restrict _).aestronglyMeasurable.convolution_integrand'      fun_prop  _ ≤ 7 * eLpNorm g 2 (volume.restrict (Ioc 0 (2 * π))) +      12 * (17 * eLpNorm g 2 (volume.restrict (Ioc 0 (2 * π)))) := by    gcongr    · rw [eLpNorm_norm]      exact eLpNorm_convolution_dirichletApprox hg    change eLpNorm ((12 : ℝ) • fun x ↦  ∫ (y : ℝ) in Ioc 0 (2 * π), ‖g y‖ * niceKernel r (x - y)) 2      (volume.restrict (Ioc 0 (2 * π))) ≤ _    rw [eLpNorm_const_smul]    gcongr    · simp [enorm]    have W := integrable_bump_convolution (f := fun x ↦ ‖g x‖) (g := fun x ↦ niceKernel r x)      hg.norm ?_ ?_ ?_ (r := r) ?_    · simpa [intervalIntegral.integral_of_le I] using W    · apply memLp_top_of_bound (by fun_prop) (r⁻¹) (Eventually.of_forall (fun y ↦ ?_))      simp [abs_of_nonneg (niceKernel_pos hr.1).le, niceKernel_le_inv]    · apply niceKernel_periodic    · exact ⟨hr.1, hr.2.trans (by linarith [Real.pi_gt_three])⟩    · simp [abs_of_nonneg (niceKernel_pos hr.1).le]  _ = 211 * eLpNorm g 2 (volume.restrict (Ioc 0 (2 * π))) := by ring  _ ≤ 2 ^ 8 * eLpNorm g 2 (volume.restrict (Ioc 0 (2 * π))) := by    gcongr    norm_num  _ = 2 ^ 8 * eLpNorm g 2 (volume.restrict (Ioc 1 4)) := by    congr 1    rw [restrict_Ioc_eq_restrict_Icc, restrict_Ioc_eq_restrict_Icc]    have : volume.restrict (Icc 1 4) = (volume.restrict (Icc 0 (2 * π))).restrict (Icc 1 4) := by      rw [Measure.restrict_restrict_of_subset]      apply Icc_subset_Icc (by norm_num) (by linarith [Real.pi_gt_three])    rw [this]    apply (eLpNorm_restrict_eq_of_support_subset h'g).symm