Source indexedlemma · leanprover/lean4:v4.32.0

intervalIntegrable_mul_dirichletKernel'

Carleson.Classical.ControlApproximationEffectBasic · Carleson/Classical/ControlApproximationEffectBasic.lean:136 to 146

Mathematical statement

Exact Lean statement

lemma intervalIntegrable_mul_dirichletKernel' {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * π)) {f : ℝ → ℂ}
    (hf : IntervalIntegrable f volume (-π) (3 * π)) {N : ℕ} :
    IntervalIntegrable (fun y ↦ f y * dirichletKernel' N (x - y)) volume (x - π) (x + π)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma intervalIntegrable_mul_dirichletKernel' {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * π)) {f : ℝ → ℂ}    (hf : IntervalIntegrable f volume (-π) (3 * π)) {N : ℕ} :    IntervalIntegrable (fun y ↦ f y * dirichletKernel' N (x - y)) volume (x - π) (x + π) := by  apply (hf.mono_set _).mul_bdd    (dirichletKernel'_measurable.comp (measurable_id.const_sub _)).aestronglyMeasurable  · use (2 * N + 1)    intro y    apply norm_dirichletKernel'_le  · rw [Set.uIcc_of_le, Set.uIcc_of_le]    on_goal 1 => apply Set.Icc_subset_Icc    all_goals linarith [hx.1, hx.2, pi_pos]