Documentation

MathlibNt.AnalyticNumberTheory.LargeSieve.DampedArctanPerronKernel

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

The exponentially damped Perron step kernel.

Equations
Instances For
    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.dampedArctanPerronKernel · compiled type and proof/definition references.

    source
    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.

    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.integral_exp_neg_mul_truncatedPerronIntegrand_eq_arctan_div · compiled type and proof/definition references.

    source
    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.

    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.dampedArctanPerronKernel_eq_half_add_integral · compiled type and proof/definition references.

    source
    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.

    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.arctan_le_self_of_nonneg · compiled type and proof/definition references.

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

    Reflection exchanges the two sides of the damped step kernel.

    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.dampedArctanPerronKernel_neg · compiled type and proof/definition references.

    source
    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|).

    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.abs_indicator_sub_dampedArctanPerronKernel_le · compiled type and proof/definition references.

    source
    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 / π.

    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.abs_halfStepIndicator_sub_dampedArctanPerronKernel_le · compiled type and proof/definition references.