Source indexedlemma · leanprover/lean4:v4.32.0

intervalIntegrable_mul_dirichletKernel'_max

Carleson.Classical.ControlApproximationEffectBasic · Carleson/Classical/ControlApproximationEffectBasic.lean:148 to 159

Mathematical statement

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma intervalIntegrable_mul_dirichletKernel'_max {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * π)) {f : ℝ → ℂ}   (hf : IntervalIntegrable f volume (-π) (3 * π)) {N : ℕ} :    IntervalIntegrable (fun y ↦ f y * ((max (1 - |x - y|) 0)      * dirichletKernel' N (x - y))) volume (x - π) (x + π) := by  conv => pattern ((f _) * _); rw [← mul_assoc]  apply intervalIntegrable_mul_dirichletKernel' hx    (IntervalIntegrable.mul_bdd hf (Complex.measurable_ofReal.comp      ((Measurable.const_sub (_root_.continuous_abs.measurable.comp        (measurable_id.const_sub _)) _).max measurable_const)).aestronglyMeasurable _)  use 1  intro y  simp [Real.norm_of_nonneg (le_max_right _ _)]