Source indexedtheorem · leanprover/lean4:v4.32.0

intervalIntegrable_sin_div_kernel_error_of_intervalIntegrable_quotient

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:546 to 567

Source documentation

Local quotient integrability gives interval-integrability of the finite sine-kernel error term.

Exact Lean statement

theorem intervalIntegrable_sin_div_kernel_error_of_intervalIntegrable_quotient
    {f : ℝ → E} {x R : ℝ}
    (hq : IntervalIntegrable
      (fun u : ℝ =>
        if u = 0 then 0 else (1 / (π * u) : ℂ) • (f (x - u) - f x))
      volume (-R) R)
    (T : ℝ) :
    IntervalIntegrable
      (fun u : ℝ =>
        (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •
          (f (x - u) - f x))
      volume (-R) R

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem intervalIntegrable_sin_div_kernel_error_of_intervalIntegrable_quotient    {f : ℝ → E} {x R : ℝ}    (hq : IntervalIntegrable      (fun u : ℝ =>        if u = 0 then 0 else (1 / (π * u) : ℂ) • (f (x - u) - f x))      volume (-R) R)    (T : ℝ) :    IntervalIntegrable      (fun u : ℝ =>        (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •          (f (x - u) - f x))      volume (-R) R := by  let q : ℝ → E := fun u =>    if u = 0 then 0 else (1 / (π * u) : ℂ) • (f (x - u) - f x)  have hsinq : IntervalIntegrable (fun u : ℝ => (Real.sin (T * u) : ℂ) • q u)      volume (-R) R := by    refine hq.continuousOn_smul ?_    fun_prop  refine hsinq.congr ?_  intro u _hu  dsimp [q]  exact (sin_div_kernel_sub_eq_sin_smul_quotient (E := E) f x T u).symm