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

Let f(z)=∑0≤k≤nϵkzkf(z)=\sum_{0\leq k\leq n} \epsilon_k z^k be a random polynomial, where ϵk∈{0,1}\epsilon_k\in \{0,1\} independently uniformly at random for 0≤k≤n0\leq k\leq n.

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

FormalConjectures/ErdosProblems/522.leanErdos522.erdos_522.variants.zero_one8 linesExact file
True ↔  ∀ {Ω : Type u_3} [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]    {n : ℕ},    1 ≤ n →      ∀ (f : Erdos522.KacCoefficients {0, 1} Ω MeasureTheory.volume),        MeasureTheory.volume            {ω | Filter.Tendsto (fun n => 2 * ↑(f.numRootsInUnitDisk n ω) / ↑n) Filter.atTop (nhds 1)} =          1
OpenStatement only, no proof