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 statement3 of 4

Yakir proved that almost all Kac polynomials have n/2+O(n^(9/10)) many roots in {z∈C:|z|≤1}.

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

1∃ p,2  Filter.Tendsto p Filter.atTop (nhds 0) ∧3    ∀ (Ω : Type u_3) [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]4      (n : ℕ),5      2 ≤ n →6        ∀ (f : Erdos522.KacCoefficients {-1, 1} Ω MeasureTheory.volume),7          (MeasureTheory.volume8                {ω |9                  |↑(Multiset.countP (fun x => x ∈ Metric.closedBall 0 1) (f.roots n ω)) - ↑n / 2| ≥10                    ↑n ^ (9 / 10)}).toReal ≤11            p n

SolvedStatement only, no proof

Sources

Search problems.science