The scaled Laplace tail of Suzuki's standard upper adjoint

The change of variables u = s * x rewrites s * p(s) as the integral of exp (-u - Ein (u / s)) over the positive half-line. Dominated convergence, using 0 ≤ Ein there, then gives the limit 1.

def MathlibNt.SieveTheory.SuzukiStandardUpperAdjointScaledTail : Prop

The elementary large-parameter Laplace asymptotic needed at infinity.

Equations

• MathlibNt.SieveTheory.SuzukiStandardUpperAdjointScaledTail = Filter.Tendsto (fun (s : ℝ) => s * MathlibNt.SieveTheory.suzukiStandardUpperAdjoint s) Filter.atTop (nhds 1)

theorem MathlibNt.SieveTheory.suzukiStandardUpperAdjoint_scaledTail : SuzukiStandardUpperAdjointScaledTail

Suzuki's genuine Laplace-integral standard upper adjoint has the elementary scaled tail s * p(s) → 1.