Source indexedlemma · leanprover/lean4:v4.32.0

eLpNorm_czOperator_restrict_two_three

Carleson.Classical.HilbertStrongType · Carleson/Classical/HilbertStrongType.lean:847 to 874

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.

Exact Lean statement

lemma eLpNorm_czOperator_restrict_two_three {g : ℝ → ℂ} {r : ℝ} (hr : r ∈ Ioo 0 1)
    (hg : MemLp g ∞ volume) :
    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 {g : ℝ → ℂ} {r : ℝ} (hr : r ∈ Ioo 0 1)    (hg : MemLp g ∞ volume) :    eLpNorm (czOperator K r g) 2 (volume.restrict (Ioc 2 3)) ≤      2 ^ 8 * eLpNorm g 2 (volume.restrict (Ioc 1 4)) := by  let g' := (indicator (Icc 1 4)) g  have A : eLpNorm g 2 (volume.restrict (Ioc 1 4)) = eLpNorm g' 2 (volume.restrict (Ioc 1 4)) := by    apply eLpNorm_congr_ae    filter_upwards [self_mem_ae_restrict measurableSet_Ioc] with y hy    simp only [g']    rw [indicator_of_mem]    exact ⟨hy.1.le, hy.2⟩  have B : eLpNorm (czOperator K r g) 2 (volume.restrict (Ioc 2 3)) =      eLpNorm (czOperator K r g') 2 (volume.restrict (Ioc 2 3)) := by    apply eLpNorm_congr_ae    filter_upwards [self_mem_ae_restrict measurableSet_Ioc] with y hy    simp only [czOperator, g']    congr with z    by_cases hz : z ∈ Icc 1 4    · rw [indicator_of_mem hz]    · suffices K y z = 0 by simp [this]      apply k_of_one_le_abs      simp only [mem_Icc, not_and, not_le] at hz      rcases lt_or_ge z 1 with h'z | h'z      · linarith [le_abs_self (y - z), hy.1]      · linarith [neg_le_abs (y - z), hy.2, hz h'z]  rw [A, B]  exact eLpNorm_czOperator_restrict_two_three_of_support_subset hr (hg.indicator measurableSet_Icc)    support_indicator_subset