The classical Euler--Ein tail asymptotic

This module proves unconditionally that

x * exp (-Ein x) -> exp (-γ)

for the Suzuki Ein used in SuzukiStandardUpperAdjoint.

theorem MathlibNt.SieveTheory.suzukiEinEulerTailAsymptotic_proof : SuzukiEinEulerTailAsymptotic

The classical Euler--Ein tail asymptotic needed to normalize Suzuki's standard upper adjoint.

theorem MathlibNt.SieveTheory.suzukiStandardUpperAdjoint_one_eq_exp_neg_eulerMascheroni_unconditional : suzukiStandardUpperAdjoint 1 = Real.exp (-Real.eulerMascheroniConstant)

The genuine Laplace adjoint has the required value at 1, with the Euler--Ein tail discharged internally rather than supplied as a premise.