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 .
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/50.leansorry ↔ ∀ (f : ℝ → ℝ), Erdos50.IsDistributionOfPhiRatio f → ¬∃ x ∈ Set.Icc 0 1, ∃ y > 0, HasDerivWithinAt f y (Set.Icc 0 1) xOpenStatement only, no proof