Source indexedlemma · leanprover/lean4:v4.32.0

integrable_cutoff_mul

Carleson.HolderVanDerCorput · Carleson/HolderVanDerCorput.lean:71 to 81

Mathematical statement

Exact Lean statement

lemma integrable_cutoff_mul {z : X} (hR : 0 < R) (ht : 0 < t) {x : X} {φ : X → ℂ}
    (hc : Continuous φ) (hφ : φ.support ⊆ ball z R) :
    Integrable (fun y ↦ cutoff R t x y * φ y)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma integrable_cutoff_mul {z : X} (hR : 0 < R) (ht : 0 < t) {x : X} {φ : X → ℂ}    (hc : Continuous φ) (hφ : φ.support ⊆ ball z R) :    Integrable (fun y ↦ cutoff R t x y * φ y) := by  apply Continuous.integrable_of_hasCompactSupport  · apply Continuous.mul    · have := cutoff_continuous hR ht (x := x)      fun_prop    · exact hc  · apply HasCompactSupport.mul_left    apply HasCompactSupport.of_support_subset_isCompact (isCompact_closedBall z R)    apply hφ.trans ball_subset_closedBall