FormalConjectures/ErdosProblems/1150.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

2 declarations, 1 contain sorry, 0 declared as axioms

Erdős Problem 1150

Reference: erdosproblems.com/1150

Imports (1)
  1. theorem Erdos1150.erdos_1150 Is there some constant sorry line 38 source

    Source documentation

    Is there some constant $c > 0$ such that, for all large enough $n$ and all polynomials $P$ of degree $n$ with coefficients in $\{-1, 1\}$, $$\max_{|z|=1} |P(z)| > (1 + c) \sqrt{n}?$$

    depends on sorry what this means

    Statement uses: Iff, True, Exists, Real, And, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, Polynomial, Complex, LE.le, Polynomial.natDegree, Or, Eq, Polynomial.coeff, Neg.neg, iSup, Metric.sphere, Norm.norm and 7 more

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

    55 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_1150 :
    answer(sorry) ↔ ∃ c > 0, ∀ᶠ n in Filter.atTop,
      ∀ P : ℂ[X],  (∀ i ≤ P.natDegree, P.coeff i = - 1 ∨ P.coeff i = 1) → P.natDegree = n →
        ⨆ z : Metric.sphere (0 : ℂ) 1, ‖P.eval (z : ℂ)‖ > (1 + c) * Real.sqrt n := by
…

    Mentions: c

  2. theorem Erdos1150.erdos_1150.variants.parseval_lower_bound The trivial lower bound from Parseval's identity: for any polynomial $P$ of degree $n$ with coefficients in $\{-1, 1\}$, we have $\max_{|z|=1} |P(z)| \geq \sqrt{n+1}$ line 54 source

    Source documentation

    The trivial lower bound from Parseval's identity: for any polynomial $P$ of degree $n$ with coefficients in $\{-1, 1\}$, we have $\max_{|z|=1} |P(z)| \geq \sqrt{n+1}$.

    This follows from Parseval's identity: $$\frac{1}{2\pi} \int_0^{2\pi} |P(e^{i\theta})|^2 d\theta = \sum_{k=0}^{n} |a_k|^2 = n+1$$ since each $|a_k|^2 = 1$. The circle average is bounded by the pointwise supremum squared, so $\max_{|z|=1} |P(z)|^2 \ge n+1$, whence $\max_{|z|=1} |P(z)| \ge \sqrt{n+1}$.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Polynomial, Complex, Nat, LE.le, Polynomial.natDegree, Or, Eq, Polynomial.coeff, Neg.neg, OfNat.ofNat, GE.ge, Real, iSup, Metric.sphere, Norm.norm, Polynomial.eval, Membership.mem, Set, Real.sqrt, HAdd.hAdd

    Proof uses: rfl, Finset, Finset.range, Iff.mp, LT.lt, Nat.succ, Nat.lt_succ_iff, Finset.mem_range, Eq.rec, Eq.symm, of_eq_true, Eq.trans, True, congrFun', congrArg, norm_neg, NormOneClass.norm_one, eq_self, Polynomial.support, Finset.ext and 72 more

    177 instances, coercions and auxiliary constants left out.

    Tactic trace: 56 steps

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

    theorem erdos_1150.variants.parseval_lower_bound (P : ℂ[X]) (n : ℕ)
    (hcoeff : ∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1)
    (hdeg : P.natDegree = n) :
    ⨆ z : Metric.sphere (0 : ℂ) 1, ‖P.eval (z : ℂ)‖ ≥ Real.sqrt (n + 1) := by
…