Erdős problem 522 · problems.science

For $P_n(z) = \sum_{k=0}^n \varepsilon_k z^k$ with independent uniform signs, does the number $R_n$ of roots in $|z| \le 1$ satisfy $R_n/(n/2) \to 1$ almost surely? The manuscript proves the strong law with $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 statement2 of 4

Erdős and Offord showed that the number of real roots of a random degree n polynomial with ±1 coefficients is (2/π+o(1))log n.

FormalConjectures/ErdosProblems/522.leanErdos522.erdos_522.variants.number_real_roots8 linesExact file

1∃ p o,2  Filter.Tendsto o Filter.atTop (nhds 0) ∧3    Filter.Tendsto p Filter.atTop (nhds 0) ∧4      ∀ (Ω : Type u_3) [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]5        (n : ℕ),6        2 ≤ n →7          ∀ (f : Erdos522.KacCoefficients {-1, 1} Ω MeasureTheory.volume),8            (MeasureTheory.volume {ω | |↑(f.roots n ω).card / Real.log ↑n - 2 / Real.pi| ≥ o n}).toReal ≤ p n

SolvedStatement only, no proof

Sources

Search problems.science