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 ∣z∣≤1|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

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

522.lean

Retained formal statement1 of 4

Let f(z)=∑0≤k≤nϵ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 0≤k≤n0\leq k\leq n.

Is it true that, if RnR_n is the number of roots of f(z)f(z) in {z∈C:∣z∣≤1}\{ z\in \mathbb{C} : \lvert z\rvert \leq 1\}, then Rnn/2→1 \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