Source indexedlemma · leanprover/lean4:v4.32.0

intervalIntegrable_mul_dirichletKernel'_specific

Carleson.Classical.ControlApproximationEffectBasic · Carleson/Classical/ControlApproximationEffectBasic.lean:213 to 224

Mathematical statement

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma intervalIntegrable_mul_dirichletKernel'_specific {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * π))    {f : ℝ → ℂ} (hf : IntervalIntegrable f volume (-π) (3 * π)) {N : ℕ} :    IntegrableOn (fun y ↦ f y * ((max (1 - |x - y|) 0)      * dirichletKernel' N (x - y))) {y | dist x y ∈ Set.Ioo 0 1} volume := by  have : IntervalIntegrable (fun y ↦ f y * ((max (1 - |x - y|) 0)      * dirichletKernel' N (x - y))) volume (x - π) (x + π) :=    intervalIntegrable_mul_dirichletKernel'_max hx hf  rw [intervalIntegrable_iff_integrableOn_Ioo_of_le (by linarith [pi_pos])] at this  apply this.mono_set  intro y hy  rw [annulus_real_eq (by rfl)] at hy  rcases hy with h | h <;> constructor <;> linarith [h.1, h.2, hx.1, hx.2, Real.two_le_pi]