Source indexedtheorem · leanprover/lean4:v4.32.0

eventually_norm_intervalIntegral_sin_div_kernel_scalar_mass_le_two

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:2076 to 2104

Source documentation

The scalar finite-window sine-kernel mass is eventually bounded by 2.

Exact Lean statement

theorem eventually_norm_intervalIntegral_sin_div_kernel_scalar_mass_le_two
    {R : ℝ} (hR : 0 < R) :
    ∀ᶠ T in Filter.atTop,
      ‖∫ u in (-R)..R,
        if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (Real.pi * u) : ℂ)‖ ≤ 2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem eventually_norm_intervalIntegral_sin_div_kernel_scalar_mass_le_two    {R : ℝ} (hR : 0 < R) :    ∀ᶠ T in Filter.atTop,      ‖∫ u in (-R)..R,        if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (Real.pi * u) : ℂ)‖ ≤ 2 := by  have hlim := tendsto_intervalIntegral_sin_div_kernel_scalar_mass hR  have hnear : ∀ᶠ T in Filter.atTop,      dist (∫ u in (-R)..R,        if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (Real.pi * u) : ℂ)) (1 : ℂ) < 1 :=    hlim.eventually (Metric.ball_mem_nhds (1 : ℂ) zero_lt_one)  filter_upwards [hnear] with T hT  have hnorm_sub : ‖(∫ u in (-R)..R,        if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (Real.pi * u) : ℂ)) -        (1 : ℂ)‖ < 1 := by    simpa [dist_eq_norm] using hT  calc    ‖∫ u in (-R)..R,        if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (Real.pi * u) : ℂ)‖        = ‖(1 : ℂ) + ((∫ u in (-R)..R,          if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (Real.pi * u) : ℂ)) -            (1 : ℂ))‖ := by          congr 1          abel    _ ≤ ‖(1 : ℂ)‖ + ‖(∫ u in (-R)..R,          if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (Real.pi * u) : ℂ)) -            (1 : ℂ)‖ := norm_add_le _ _    _ ≤ 2 := by      norm_num at hnorm_sub ⊢      linarith