Source indexedlemma · leanprover/lean4:v4.32.0

integrableOn_coi_inner_annulus'

Carleson.MetricCarleson.Basic · Carleson/MetricCarleson/Basic.lean:279 to 289

Source documentation

The integrand of carlesonOperatorIntegrand is integrable over the R₁, R₂ annulus.

Exact Lean statement

lemma integrableOn_coi_inner_annulus' (nf : IntegrableOn f (Annulus.oo x R₁ R₂)) (hR₁ : 0 < R₁) :
    IntegrableOn (fun y ↦ K x y * f y * exp (I * θ y)) (Annulus.oo x R₁ R₂)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma integrableOn_coi_inner_annulus' (nf : IntegrableOn f (Annulus.oo x R₁ R₂)) (hR₁ : 0 < R₁) :    IntegrableOn (fun y ↦ K x y * f y * exp (I * θ y)) (Annulus.oo x R₁ R₂) := by  simp_rw [mul_assoc]; refine integrableOn_K_mul ?_ _ hR₁ fun y my ↦ ?_  · conv => congr; ext y; rw [mul_comm]    rw [IntegrableOn]    apply nf.bdd_mul (c := 1)    · exact ((Complex.measurable_ofReal.comp (by fun_prop)).const_mul I).cexp.aestronglyMeasurable    · refine ae_of_all _ fun x => ?_      rw [mul_comm, norm_exp_ofReal_mul_I]  · rw [Annulus.oo, mem_setOf, mem_Ioo] at my    rw [mem_compl_iff, mem_ball', not_lt]; exact my.1.le