FormalConjectures/ErdosProblems/1133.lean

GitHub source file

2 declarations, 2 contain sorry, 0 declared as axioms

1. theorem Erdos1133.erdos_1133 Let $C>0$ sorry line 47 source

   Source documentation

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

   Yang [Ya26, Theorem 2.1] proved this, including repeated nodes, by taking $\rho=0$.

   depends on sorry what this means

   Statement uses: Iff, True, Real, GT.gt, OfNat.ofNat, Exists, And, Filter.Eventually, Nat, Fin, Set.Icc, Neg.neg, Polynomial, LT.lt, Polynomial.natDegree, HMul.hMul, HAdd.hAdd, GE.ge, Finset.card, Finset.filter and 8 more

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   51 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_1133 :
       answer(True) ↔
       ∀ C > (0 : ℝ), ∃ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
         ∀ x : Fin n → Icc (-1 : ℝ) 1,
           ∃ y : Fin n → Icc (-1 : ℝ) 1,
             ∀ P : Polynomial ℝ,
               (P.natDegree : ℝ) < (1 + ε) * (n : ℝ) →
               ((Finset.univ.filter (fun i ↦ P.eval (x i : ℝ) = (y i : ℝ))).card : ℝ) ≥
                 (1 - ε) * (n : ℝ) →
               ∃ z ∈ Icc (-1 : ℝ) 1, |P.eval z| > C := by
   …

2. theorem Erdos1133.erdos_1133.variants.weaker Documented declaration: weaker sorry line 67 source

   Source documentation

   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 robust interpolation statement above also implies this result. Erdős in [Er67] could not prove the robust statement even for $m=n$.

   depends on sorry what this means

   Statement uses: Real, GT.gt, OfNat.ofNat, Exists, And, Filter.Eventually, Nat, Nat.floor, HMul.hMul, HAdd.hAdd, Fin, Set.Icc, Neg.neg, Polynomial, Eq, Polynomial.natDegree, LE.le, abs, Polynomial.eval, Membership.mem and 2 more

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   53 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_1133.variants.weaker :
       ∀ C > (0 : ℝ), ∃ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
         let m := ⌊(1 + ε) * (n : ℝ)⌋₊;
   …