erdos_1038.inf_lowerBound

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 `≥ 2 ^ (4 / 3) - 1`.

theorem erdos_1038.inf_lowerBound (n : ℕ) : 2 ^ (4 / 3 : ℝ) - 1 ≤
    ⨅ 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}

Recent Submissions

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