Skip to content

Erdős problem 522

For Pn(z)=k=0nεkzkP_n(z) = \sum_{k=0}^n \varepsilon_k z^k with independent uniform signs, does the number RnR_n of roots in z1|z| \le 1 satisfy Rn/(n/2)1R_n/(n/2) \to 1 almost surely? The manuscript proves the strong law with Rn=n/2+Oω(n149/150)R_n = n/2 + O_\omega(n^{149/150}).

Sources

Browse retained paths and inspect the exact material available for this Problem.

5 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

522.lean

Retained formal statement1 of 4

Let f(z)=0knϵkzkf(z)=\sum_{0\leq k\leq n} \epsilon_k z^k be a random polynomial, where ϵk{1,1}\epsilon_k\in \{-1,1\} independently uniformly at random for 0kn0\leq k\leq n.

Is it true that, if RnR_n is the number of roots of f(z)f(z) in {zC:z1}\{ z\in \mathbb{C} : \lvert z\rvert \leq 1\}, then Rnn/21 \frac{R_n}{n/2}\to 1 almost surely?

There is some ambiguity as to whether the intended coefficient set is {1,1}\{-1, 1\} or {0,1}\{0, 1\}, see erdos_522.variants.zero_one for the alternate version.

FormalConjectures/ErdosProblems/522.leanErdos522.erdos_5224 linesExact file
True  ∀ {Ω : Type u_3} [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]    (c : Erdos522.KacCoefficients {-1, 1} Ω MeasureTheory.volume),    MeasureTheory.volume {ω | Filter.Tendsto (fun n => 2 * ↑(c.numRootsInUnitDisk n ω) / ↑n) Filter.atTop (nhds 1)} = 1
OpenStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page