erdos_1038.sup

The supremum of `|{x ∈ ℝ : |f x| < 1}|` over all monic polynomials `f` such that all of its roots are real and contained in `[-1,1]` is `2 * 2 ^ (1 / 2)`. This is proved in [Tao25].

theorem erdos_1038.sup (n : ℕ) : 2 * 2 ^ (1 / 2 : ℝ) =
    ⨆ f : {f : Polynomial ℝ // f.Monic ∧
    (f.roots.filter fun x => x ∈ Set.Icc (-1 : ℝ) 1).card = f.natDegree},
    volume {x | |f.1.eval x| < 1}

Recent Submissions

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