Skip to content

Erdős problem 522

Start work

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 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
∃ p o,  Filter.Tendsto o Filter.atTop (nhds 0) ∧    Filter.Tendsto p Filter.atTop (nhds 0) ∧      ∀ (Ω : Type u_3) [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]        (n : ℕ),        2 ≤ n →          ∀ (f : Erdos522.KacCoefficients {-1, 1} Ω MeasureTheory.volume),            (MeasureTheory.volume {ω | |↑(f.roots n ω).card / Real.log ↑n - 2 / Real.pi| ≥ o n}).toReal ≤ p n
SolvedStatement only, no proof