The classical Euler--Ein tail asymptotic #
This module proves unconditionally that
x * exp (-Ein x) -> exp (-γ)
for the Suzuki Ein used in SuzukiStandardUpperAdjoint.
The classical Euler--Ein tail asymptotic needed to normalize Suzuki's standard upper adjoint.
Inspect dependencies
MathlibNt.SieveTheory.suzukiEinEulerTailAsymptotic_proof · compiled type and proof/definition references.
theorem
MathlibNt.SieveTheory.suzukiStandardUpperAdjoint_one_eq_exp_neg_eulerMascheroni_unconditional :
The genuine Laplace adjoint has the required value at 1, with the
Euler--Ein tail discharged internally rather than supplied as a premise.
Inspect dependencies
MathlibNt.SieveTheory.suzukiStandardUpperAdjoint_one_eq_exp_neg_eulerMascheroni_unconditional · compiled type and proof/definition references.