Source indexedtheorem · leanprover/lean4:v4.32.0

integrable_tile_sum_operator

Carleson.FinitaryCarleson · Carleson/FinitaryCarleson.lean:16 to 26

Mathematical statement

Exact Lean statement

theorem integrable_tile_sum_operator
    {f : X → ℂ} (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x) {x : X} {s : ℤ} :
    Integrable fun y ↦ Ks s x y * f y * exp (I * (Q x y - Q x x))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem integrable_tile_sum_operator    {f : X → ℂ} (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x) {x : X} {s : ℤ} :    Integrable fun y ↦ Ks s x y * f y * exp (I * (Q x y - Q x x)) := by  simp_rw [mul_assoc, mul_comm (Ks s x _)]  refine integrable_Ks_x (one_lt_realD X) |>.bdd_mul (c := 1) ?_ (ae_of_all _ fun y ↦ ?_)  · exact hf.mul ((measurable_ofReal.comp (map_continuous (Q x)).measurable |>.sub      measurable_const).const_mul I).cexp |>.aestronglyMeasurable  · rw [norm_mul, ← one_mul 1]    gcongr    · exact le_trans (h2f y) (F.indicator_le_self' (by simp) y)    · rw_mod_cast [mul_comm, norm_exp_ofReal_mul_I]