Erdős Problem 1133

References:

• erdosproblems.com/1133
• [Er67] Erdős, P., Problems and results on the convergence and divergence properties of the Lagrange interpolation polynomials and some extremal problems. Mathematica (Cluj) (1967), 65-73.

theorem Erdos1133.erdos_1133 : sorry ↔ ∀ C > 0, ∃ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (x : Fin n → ↑(Set.Icc (-1) 1)), ∃ (y : Fin n → ↑(Set.Icc (-1) 1)), ∀ (P : Polynomial ℝ), ↑P.natDegree < (1 + ε) * ↑n → ↑{i : Fin n | Polynomial.eval (↑(x i)) P = ↑(y i)}.card ≥ (1 - ε) * ↑n → ∃ z ∈ Set.Icc (-1) 1, |Polynomial.eval z P| > C

Let $C>0$. There exists $\epsilon>0$ such that if $n$ is sufficiently large the following holds.

For any $x_1,\ldots,x_n\in [-1,1]$ there exist $y_1,\ldots,y_n\in [-1,1]$ such that, if $P$ is a polynomial of degree $m<(1+\epsilon)n$ with $P(x_i)=y_i$ for at least $(1-\epsilon)n$ many $1\leq i\leq n$, then [\max_{x\in [-1,1]}\lvert P(x)\rvert >C.]

theorem Erdos1133.erdos_1133.variants.weaker (C : ℝ) : C > 0 → ∃ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, have m := ⌊(1 + ε) * ↑n⌋₊; ∀ (x : Fin m → ↑(Set.Icc (-1) 1)), ∃ (P : Polynomial ℝ), P.natDegree = n ∧ (∀ (i : Fin m), |Polynomial.eval (↑(x i)) P| ≤ 1) ∧ ∃ z ∈ Set.Icc (-1) 1, |Polynomial.eval z P| > C

Erdős proved that, for any $C>0$, there exists $\epsilon>0$ such that if $n$ is sufficiently large and $m=\lfloor (1+\epsilon)n\rfloor$ then for any $x_1,\ldots,x_m\in [-1,1]$ there is a polynomial $P$ of degree $n$ such that $\lvert P(x_i)\rvert\leq 1$ for $1\leq i\leq m$ and $\max_{x\in [-1,1]}\lvert P(x)\rvert>C$. The conjectured statement would also imply this, but Erdős in [Er67] says he could not even prove it for $m=n$.