Erdős problem 1038 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

5 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1038.lean

Retained formal statement3 of 4

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.

FormalConjectures/ErdosProblems/1038.leanErdos1038.erdos_1038.varaints.inf_lowerBound1 lineExact file

1∀ (n : ℕ), 2 ^ (4 / 3) - 1 ≤ ⨅ f, MeasureTheory.volume {x | |Polynomial.eval x ↑f| < 1}

SolvedStatement only, no proof

Sources

Search problems.science