Erdős problem 50
Schoenberg [Sch38] proved that the asymptotic distribution function of exists. That is, for any , the proportion of integers satisfying approaches a limit as . This limit function is the cumulative distribution function of the values of .
Sources
FormalConjectures/ErdosProblems/
50.lean
Retained formal statement
Schoenberg [Sch38] proved that the asymptotic distribution function of exists. That is, for any , the proportion of integers satisfying approaches a limit as . This limit function is the cumulative distribution function of the values of .
∃ f, Erdos50.IsDistributionOfPhiRatio fSolvedStatement only, no proof