OAI/NumberTheory/JointDickman/Amplification/BinMarginalInput.lean

The published one-variable distribution input

G. Tenenbaum, A rate estimate in Billingsley's theorem for the size distribution of large prime factors, Quart. J. Math. 51 (2000), 385–403: the unnumbered main Theorem, parts (i), (iii) at H = 0, equations (1.1), (1.3), and the multiplicity remark following (1.7), printed pp. 386–388. Author's corrected version: https://tenenb.perso.math.cnrs.fr/PPP/Billingsley.pdf

The input below is only its finite-bin consequence. Thresholds are the fixed positive numbers k/J; hence finitely many ranks suffice. Continuity of the limiting distribution permits replacing the counting endpoint by A*x and the rank thresholds by powers of x. Its first-rank marginal is the classical Dickman law. No statement about two different integers, residue restrictions, weights, or short intervals is included.