Source indexedtheorem · leanprover/lean4:v4.32.0

sin_div_error_pointwise_bound

PrimeNumberTheoremAnd.SincKernelErrorBounds · PrimeNumberTheoremAnd/SincKernelErrorBounds.lean:21 to 56

Source documentation

Pointwise bound on the sin-div windowed error term: scaling by the normalized sinc kernel and a mean-value estimate on g (x - u) - g x gives a bound D / π that is independent of the height T.

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem sin_div_error_pointwise_bound    {g : ℝ → ℂ} {D x T u : ℝ}    (hD : 0 ≤ D) (hgdiff : Differentiable ℝ g)    (hderiv : ∀ y : ℝ, ‖deriv g y‖ ≤ D) :    ‖(if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (Real.pi * u) : ℂ)) •        (g (x - u) - g x)‖ ≤ D / Real.pi := by  by_cases hu : u = 0  · simp [hu, div_nonneg hD Real.pi_pos.le]  · rw [if_neg hu, norm_smul]    have hscalar :        ‖(Real.sin (T * u) / (Real.pi * u) : ℂ)‖ ≤ 1 / (Real.pi * |u|) := by      rw [norm_div, norm_mul, Complex.norm_real, Complex.norm_real, Complex.norm_real]      simp only [Real.norm_eq_abs]      rw [abs_of_pos Real.pi_pos]      have hsin : |Real.sin (T * u)| ≤ 1 := Real.abs_sin_le_one _      exact div_le_div_of_nonneg_right hsin        (mul_nonneg Real.pi_pos.le (abs_nonneg u))    have hdiff : ‖g (x - u) - g x‖ ≤ D * |u| := by      have hmv :=        (convex_univ : Convex ℝ (Set.univ : Set ℝ)).norm_image_sub_le_of_norm_deriv_le          (f := g) (C := D)          (fun y _hy => hgdiff y)          (fun y _hy => hderiv y)          (x := x) (y := x - u) (by simp) (by simp)      have hnorm : ‖(x - u) - x‖ = |u| := by        rw [Real.norm_eq_abs]        have hsub : (x - u) - x = -u := by ring        rw [hsub, abs_neg]      simpa [hnorm] using hmv    have hupper_nonneg : 0 ≤ 1 / (Real.pi * |u|) := by positivity    calc      ‖(Real.sin (T * u) / (Real.pi * u) : ℂ)‖ * ‖g (x - u) - g x‖          ≤ (1 / (Real.pi * |u|)) * (D * |u|) := by            exact mul_le_mul hscalar hdiff (norm_nonneg _) hupper_nonneg      _ = D / Real.pi := by            field_simp [Real.pi_ne_zero, abs_pos.mpr hu]