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

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

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

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

FormalConjectures/ErdosProblems/522.leanErdos522.erdos_5224 linesExact file

1True ↔2  ∀ {Ω : Type u_3} [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]3    (c : Erdos522.KacCoefficients {-1, 1} Ω MeasureTheory.volume),4    MeasureTheory.volume {ω | Filter.Tendsto (fun n => 2 * ↑(c.numRootsInUnitDisk n ω) / ↑n) Filter.atTop (nhds 1)} = 1

OpenStatement only, no proof

Sources

Search problems.science