LineSmoothCarleson.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The local and far parts of the actual smooth projection Carleson estimate on a finite dyadic scale range.

theorem OAI.LipschitzHilbert.PacketRepresentation.lineConvolution_indicator_split line 13
theorem OAI.LipschitzHilbert.PacketRepresentation.lineProjection_far_integrable line 33

theorem OAI.LipschitzHilbert.PacketRepresentation.lineProjection_smooth_carleson line 49

Source documentation

A bounded function produces a Carleson square sum for any fixed smooth annular window having the indicated finite Fourier square bound.

theorem lineProjection_smooth_carleson (q : SchwartzMap ℝ ℂ) (N : ℕ)
    (a b : ℝ) (hab : a<b) (M : ℝ) (hM : 0≤M)
    (hframe : ∀ eta, (∑ n∈Finset.range N,
      ‖q (((b-a)/(2:ℝ)^n)*eta)‖^2)≤M)
    (f : ℝ → ℂ) (hfm : Measurable f) (B : ℝ) (hB : 0≤B)
    (hfb : ∀ x, ‖f x‖≤B) :
    (∑ n∈Finset.range N, ∫ x in Icc a b,
      ‖lineConvolution (lineProjectionKernel q ((b-a)/(2:ℝ)^n)
        (by positivity)) f x‖^2)≤
      (6*M+4*(∫ t, |t| *‖(𝓕⁻ q : SchwartzMap ℝ ℂ) t‖)^2)*B^2*(b-a) := by
…

Mentions: OAI.LipschitzHilbert.PacketRepresentation.lineConvolution, OAI.LipschitzHilbert.PacketRepresentation.lineProjectionKernel