OAI/NumberTheory/TotientAsymptotic/PublishedConcentration.lean

The fixed-deviation consequence of Ford, The distribution of totients, arXiv:1104.3264v2 (2013), Lemma 6.1, (6.6)--(6.8), pp. 30--31. We use deviation 1/40 only. For the lower tail take theta = (1/40)/(1-1/40) in (6.6); for the upper tail take theta = -(1/40)/(1+1/40) in (6.7) or (6.8), splitting at -i*lambda_i/L. The uniform bounds (6.4) give positive absolute constants in exp (-c*(L-i)). Letting the terminal cutoff decrease to zero and rescaling the simplex gives precisely the input below. The transfer from Ford's terminal coefficient 1 to our coefficient a_1 is proved here using shrinkLast, rather than assumed in this input.