Source indexedtheorem · leanprover/lean4:v4.32.0

intervalIntegral_sin_div_kernel_split

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:896 to 947

Source documentation

Finite symmetric-window split for the sin (T * u) / (π * u) kernel. This is the valid algebraic surface for the principal-value mass term before taking an improper limit.

Exact Lean statement

theorem intervalIntegral_sin_div_kernel_split
    [CompleteSpace E]
    (f : ℝ → E) (x T R : ℝ)
    (hconst : IntervalIntegrable
      (fun u : ℝ =>
        (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) • f x)
      volume (-R) R)
    (herr : IntervalIntegrable
      (fun u : ℝ =>
        (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •
          (f (x - u) - f x))
      volume (-R) R) :
    (∫ u in (-R)..R,
        (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •
          f (x - u)) =
      (∫ u in (-R)..R,
        if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) • f x +
        ∫ u in (-R)..R,
          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •
            (f (x - u) - f x)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem intervalIntegral_sin_div_kernel_split    [CompleteSpace E]    (f : ℝ → E) (x T R : ℝ)    (hconst : IntervalIntegrable      (fun u : ℝ =>        (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) • f x)      volume (-R) R)    (herr : IntervalIntegrable      (fun u : ℝ =>        (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •          (f (x - u) - f x))      volume (-R) R) :    (∫ u in (-R)..R,        (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •          f (x - u)) =      (∫ u in (-R)..R,        if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) • f x +        ∫ u in (-R)..R,          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •            (f (x - u) - f x) := by  calc    (∫ u in (-R)..R,        (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •          f (x - u))        = ∫ u in (-R)..R,          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) • f x +            (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •              (f (x - u) - f x) := by          apply intervalIntegral.integral_congr          intro u _hu          change            (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •                f (x - u) =              (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) • f x +                (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •                  (f (x - u) - f x)          rw [show f (x - u) = f x + (f (x - u) - f x) by abel]          rw [smul_add]          congr 1          abel_nf    _ = (∫ u in (-R)..R,          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) • f x) +        ∫ u in (-R)..R,          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •            (f (x - u) - f x) := by          rw [intervalIntegral.integral_add hconst herr]    _ = (∫ u in (-R)..R,        if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) • f x +        ∫ u in (-R)..R,          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •            (f (x - u) - f x) := by          rw [intervalIntegral.integral_smul_const]