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

Let $f(z)=\sum_{0\leq k\leq n} \epsilon_k z^k$ be a random polynomial, where $\epsilon_k\in \{0,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?

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

1True ↔2  ∀ {Ω : Type u_3} [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]3    {n : ℕ},4    1 ≤ n →5      ∀ (f : Erdos522.KacCoefficients {0, 1} Ω MeasureTheory.volume),6        MeasureTheory.volume7            {ω | Filter.Tendsto (fun n => 2 * ↑(f.numRootsInUnitDisk n ω) / ↑n) Filter.atTop (nhds 1)} =8          1

OpenStatement only, no proof

Sources

Search problems.science