OAI.TotientAsymptotic.totient_asymptotic_formula

The theorem states a four-part asymptotic result about the number V(x) of totient values (positive integers v of the form φ(n) with n>0) that are at most x. Here, with a(j)=(j+1)log(j+1)−j log j−1, ρ is the infimum of the set of z in (0,1) with Σ_{j≥0} a(j+1) z^{j+1}=1, λ=log(1/ρ), and γ is the reciprocal of Σ (j+1)a(j+1)ρ^{j+1}. For each s, α(s)=λe^{λs}. AH(H,f,s) is a finite-level expression built from ρ, γ/α(s), the least-preimage function ell(d) (the smallest n with φ(n)=d, or 0 if none), and inclusion-exclusion sums over finite sets of tail-prime data satisfying a witness condition. A(f,s) is its limit as H tends to infinity, taken with Lean's limUnder, which returns an arbitrary value if no limit exists. The main term is x/log x · G(x,m(x)) · A(1, θ(x)), where G, m and θ are explicit auxiliary quantities built from B(x)=log log x. Writing 1 for the constant function, the conclusion has four parts. First, AH(H,1,·) converges uniformly to A(1,·) as H→∞ on the interval [0,1). Second, there are real constants cMinus>0 and cPlus such that cMinus ≤ A(1,s) ≤ cPlus for every s in [0,1). Third, V(x)/mainTerm(x) tends to 1 as x→∞. Fourth, for every c>0, V(cx)/V(x) tends to c as x→∞. The proof is admitted in the source.