Erdős problem 1133
Must every sufficiently large node set admit bounded labels that force any polynomial fitting almost all labels at degree below to have arbitrarily large uniform norm? Claimed via Beurling density for Bernstein spaces.
Sources
FormalConjectures/ErdosProblems/
1133.lean
Retained formal statement
Erdős proved that, for any , there exists such that if is sufficiently large and then for any there is a polynomial of degree such that for and . The conjectured statement would also imply this, but Erdős in [Er67] says he could not even prove it for .
∀ C > 0, ∃ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, have m := ⌊(1 + ε) * ↑n⌋₊; ∀ (x : Fin m → ↑(Set.Icc (-1) 1)), ∃ P, P.natDegree = n ∧ (∀ (i : Fin m), |Polynomial.eval (↑(x i)) P| ≤ 1) ∧ ∃ z ∈ Set.Icc (-1) 1, |Polynomial.eval z P| > CSolvedStatement only, no proof