Skip to content

Erdős problem 1038

Among all nonconstant monic polynomials ff whose roots lie in [−1,1][-1, 1], determine inf⁡f∣{x∈R:∣f(x)∣<1}∣\inf_f |\{x \in \mathbb{R} : |f(x)| < 1\}|.

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1038.lean

Retained formal statement2 of 4

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

FormalConjectures/ErdosProblems/1038.leanErdos1038.erdos_1038.parts.ii1 lineExact file
∀ (n : ℕ), 2 * 2 ^ (1 / 2) = ⨆ f, MeasureTheory.volume {x | |Polynomial.eval x ↑f| < 1}
SolvedStatement only, no proof