Erdős Problem 1038

Reference:

• erdosproblems.com/1038
• [Tao25] Tao, Terence. Sublevel Sets of Logarithmic Potentials. Terry Tao’s Blog, Dec. 2025 (https://terrytao.wordpress.com/wp-content/uploads/2025/12/erdos-1038-1.pdf)

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

What is 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]?

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

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 Erdos1038.erdos_1038.inf_lowerBound (n : ℕ) : 2 ^ (4 / 3) - 1 ≤ ⨅ (f : { f : Polynomial ℝ // f.Monic ∧ f ≠ 1 ∧ (Multiset.filter (fun (x : ℝ) => x ∈ Set.Icc (-1) 1) f.roots).card = f.natDegree }), MeasureTheory.volume {x : ℝ | |Polynomial.eval x ↑f| < 1}

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

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].