erdos_1038.inf_upperBound

The infimum of `|{x ∈ ℝ : |f x| < 1}|` over all nonconstant monic polynomials `f` such that all of its roots are real and contained in `[-1,1]` is `< 1.835`.

theorem erdos_1038.inf_upperBound (n : ℕ) : ⨅ f : {f : Polynomial ℝ // f.Monic ∧ f ≠ 1 ∧
    (f.roots.filter fun x => x ∈ Set.Icc (-1 : ℝ) 1).card = f.natDegree},
    volume {x | |f.1.eval x| < 1} < 1.835

Recent Submissions

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