Source indexedlemma · leanprover/lean4:v4.32.0

eLpNorm_czOperator_restrict

Carleson.Classical.HilbertStrongType · Carleson/Classical/HilbertStrongType.lean:879 to 903

Source documentation

The operator czOperator K r is bounded from L^2 [a - 1, a + 2] to L^2 [a, a + 1], uniformly in r and a. This follows from the same fact from L^2 [1, 4] to L^2 [2, 3] proved using Fourier series, and translation invariance.

Exact Lean statement

lemma eLpNorm_czOperator_restrict {g : ℝ → ℂ} {r a : ℝ} (hr : r ∈ Ioo 0 1)
    (hg : MemLp g ∞ volume) :
    eLpNorm (czOperator K r g) 2 (volume.restrict (Ioc a (a + 1))) ≤
      2 ^ 8 * eLpNorm g 2 (volume.restrict (Ioc (a - 1) (a + 2)))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma eLpNorm_czOperator_restrict {g : ℝ → ℂ} {r a : ℝ} (hr : r ∈ Ioo 0 1)    (hg : MemLp g ∞ volume) :    eLpNorm (czOperator K r g) 2 (volume.restrict (Ioc a (a + 1))) ≤      2 ^ 8 * eLpNorm g 2 (volume.restrict (Ioc (a - 1) (a + 2))) := by  let g' := g ∘ (fun x ↦ x + (a - 2))  have A : eLpNorm g 2 (volume.restrict (Ioc (a - 1) (a + 2))) =      eLpNorm g' 2 (volume.restrict (Ioc 1 4)) := by    rw [eLpNorm_comp_measurePreserving (hg.restrict _).aestronglyMeasurable]    have : MeasurePreserving (fun x ↦ x + (a - 2)) := measurePreserving_add_right volume (a - 2)    convert! this.restrict_preimage (s := Ioc (a - 1) (a + 2)) measurableSet_Ioc    simp    norm_num  have B : eLpNorm (czOperator K r g) 2 (volume.restrict (Ioc a (a + 1))) =      eLpNorm (czOperator K r g') 2 (volume.restrict (Ioc 2 3)) := by    have : czOperator K r g' = (czOperator K r g) ∘ (fun x ↦ x + (a - 2)) := by      rw [K_def, ← czOperator_comp_add]    rw [this, eLpNorm_comp_measurePreserving]    · apply AEStronglyMeasurable.restrict      apply czOperator_aestronglyMeasurable' Hilbert_kernel_measurable hg.aestronglyMeasurable    · convert! (measurePreserving_add_right volume (a - 2)).restrict_preimage measurableSet_Ioc      simp      norm_num  rw [A, B]  apply eLpNorm_czOperator_restrict_two_three hr  exact hg.comp_measurePreserving (measurePreserving_add_right volume (a - 2))