Skip to content

Erdős problem 521

Let (ϵk)k≥0(\epsilon_k)_{k\geq 0} be independently uniformly chosen at random from {−1,1}\{-1,1\}. If RnR_n counts the number of real roots of fn(z)=∑0≤k≤nϵkzkf_n(z)=\sum_{0\leq k\leq n}\epsilon_k z^k then is it true that, almost surely, lim⁡n→∞Rnlog⁡n=2π?\lim_{n\to \infty}\frac{R_n}{\log n}=\frac{2}{\pi}?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

521.lean

Retained formal statement2 of 3

fairCoin gives each of the two signs mass 1/2. Together with fairCoin_isProbabilityMeasure this pins the definition down, so a proof stating the same problem with a Bernoulli(1/2) measure is stating the same thing.

FormalConjectures/ErdosProblems/521.leanErdos521.fairCoin_apply1 lineExact file
∀ (b : Bool), Erdos521.fairCoin {b} = 2⁻¹
APIStatement only, no proofformal statement reference