erdos_522.variants.yakir_solution

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

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

Recent Submissions

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