noncomputable def AnalyticNumberTheory.LargeSieve.dampedArctanPerronKernel (ε x : ℝ) : ℝ

The exponentially damped Perron step kernel.

Equations

• AnalyticNumberTheory.LargeSieve.dampedArctanPerronKernel ε x = 1 / 2 + Real.arctan (x / ε) / Real.pi

theorem AnalyticNumberTheory.LargeSieve.integral_exp_neg_mul_truncatedPerronIntegrand_eq_arctan_div (ε x : ℝ) (hε : 0 < ε) : ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-ε * t) * truncatedPerronIntegrand x t = Real.arctan (x / ε)

The damped removable sine kernel integrates exactly to arctan (x / ε). The proof handles positive, negative, and zero frequencies.

theorem AnalyticNumberTheory.LargeSieve.dampedArctanPerronKernel_eq_half_add_integral (ε x : ℝ) (hε : 0 < ε) : dampedArctanPerronKernel ε x = 1 / 2 + 1 / Real.pi * ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-ε * t) * truncatedPerronIntegrand x t

The exact Ioi integral representation of the damped kernel.

theorem AnalyticNumberTheory.LargeSieve.arctan_le_self_of_nonneg {z : ℝ} (hz : 0 ≤ z) : Real.arctan z ≤ z

On the nonnegative half-line, arctan lies below the identity.

theorem AnalyticNumberTheory.LargeSieve.dampedArctanPerronKernel_neg (ε x : ℝ) : dampedArctanPerronKernel ε (-x) = 1 - dampedArctanPerronKernel ε x

Reflection exchanges the two sides of the damped step kernel.

theorem AnalyticNumberTheory.LargeSieve.abs_indicator_sub_dampedArctanPerronKernel_le {ε x : ℝ} (hε : 0 < ε) (hx : x ≠ 0) : |(if 0 < x then 1 else 0) - dampedArctanPerronKernel ε x| ≤ ε / (Real.pi * |x|)

Away from the jump, exponential damping approximates the strict indicator with the sharp elementary error ε / (π |x|).

theorem AnalyticNumberTheory.LargeSieve.abs_halfStepIndicator_sub_dampedArctanPerronKernel_le {ε : ℝ} {n Y M : ℕ} (hε : 0 < ε) (hn : n ≠ 0) (hM : 1 ≤ M) (hYM : Y ≤ M) : |(if n ≤ Y then 1 else 0) - dampedArctanPerronKernel ε (Real.log (MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep Y / ↑n))| ≤ 8 * ε * ↑M / Real.pi

At an integer half-step, the logarithmic separation converts the pointwise damped-kernel error into the uniform bound 8 ε M / π.