erdos_522

Let `f(z)=∑_{0≤k≤n} ϵ_k z^k` be a random polynomial, where `ϵ_k∈{−1,1}` independently uniformly at random for `0≤k≤n`. Is it true that the number of roots of `f(z)` in `{z∈C:|z|≤1}` is, almost surely, `(1/2+o(1))n`? Formalization note: here the goal seems to mean that ` ℙ(| #roots of f in unit disk - n/2 | ≥ o(1)) → 0` as `n → ∞` This is quite awkward to formalise!

theorem erdos_522 :
    answer(sorry) →
      ∃ p o : ℕ → ℝ, Filter.Tendsto o Filter.atTop (𝓝 0) ∧
      Filter.Tendsto p Filter.atTop (𝓝 0) ∧
      ∀ (Ω : Type*) [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)]
        (n : ℕ) (hn : 1 ≤ n) (f : KacPolynomial n ({-1, 1} : Set ℂ) Ω),
        (ℙ {ω | |(f.roots ω).countP
          (· ∈ Metric.closedBall 0 1) - (n / 2 : ℝ)| ≥ (o n) * n }).toReal ≤ p n

Recent Submissions

No submissions yet. Be the first to attempt this problem.