Source indexedtheorem · leanprover/lean4:v4.32.0

sin_div_error_interval_bound

PrimeNumberTheoremAnd.SincKernelErrorBounds · PrimeNumberTheoremAnd/SincKernelErrorBounds.lean:60 to 74

Source documentation

Interval form of sin_div_error_pointwise_bound: integrating the pointwise bound over [-1, 1] controls the windowed error integral by (D / π) · vol (Ioc (-1) 1).

Exact Lean statement

theorem sin_div_error_interval_bound
    {g : ℝ → ℂ} {D x T : ℝ}
    (hD : 0 ≤ D) (hgdiff : Differentiable ℝ g)
    (hderiv : ∀ y : ℝ, ‖deriv g y‖ ≤ D) :
    ‖∫ u in (-(1 : ℝ))..(1 : ℝ),
        (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (Real.pi * u) : ℂ)) •
          (g (x - u) - g x)‖ ≤
      (D / Real.pi) * (volume.real (Set.Ioc (-(1 : ℝ)) (1 : ℝ)))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem sin_div_error_interval_bound    {g : ℝ → ℂ} {D x T : ℝ}    (hD : 0 ≤ D) (hgdiff : Differentiable ℝ g)    (hderiv : ∀ y : ℝ, ‖deriv g y‖ ≤ D) :    ‖∫ u in (-(1 : ℝ))..(1 : ℝ),        (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (Real.pi * u) : ℂ)) •          (g (x - u) - g x)‖ ≤      (D / Real.pi) * (volume.real (Set.Ioc (-(1 : ℝ)) (1 : ℝ))) := by  rw [intervalIntegral.integral_of_le (by norm_num : (-(1 : ℝ)) ≤ 1)]  refine norm_setIntegral_le_of_norm_le_const (μ := volume)    (s := Set.Ioc (-(1 : ℝ)) (1 : ℝ)) ?_ ?_  · simp [Real.volume_Ioc]  · intro u _hu    exact sin_div_error_pointwise_bound (g := g) (D := D) (x := x) (T := T) (u := u)      hD hgdiff hderiv