FormalConjectures/ErdosProblems/510.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

3 declarations, 3 contain sorry, 0 declared as axioms

Erdős Problem 510

References:

Imports (1)
Imported by 1 file
  1. theorem Erdos510.erdos_510 Documented declaration: erdos_510 sorry line 45 source

    Source documentation

    Chowla's cosine problem

    If $A\subset \mathbb{N}$ is a finite set of positive integers of size $N > 0$ then is there some absolute constant $c>0$ and $\theta$ such that $$\sum_{n\in A}\cos(n\theta) < -cN^{1/2}?$$

    depends on sorry what this means

    Statement uses: Iff, True, Exists, Real, LT.lt, OfNat.ofNat, Filter.Eventually, Nat, Finset, Not, Membership.mem, Eq, Finset.card, Finset.sum, Real.cos, HMul.hMul, Neg.neg, Real.sqrt, Filter.atTop

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

    26 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_510 :
    answer(sorry) ↔ ∃ (c : ℝ) (hc : 0 < c),
      ∀ᶠ N in atTop, ∀ (A : Finset ℕ), 0 ∉ A → #A = N →
      ∃ θ, ∑ n ∈ A, cos (n * θ) < -c * sqrt N := by
…

    Mentions: c

  2. theorem Erdos510.erdos_510.variants.ruzsa Ruzsa [Ru04] proved an upper bound of $-\exp(O(\sqrt{\log N})$ sorry line 55 source

    Source documentation

    Ruzsa [Ru04] proved an upper bound of $-\exp(O(\sqrt{\log N})$.

    depends on sorry what this means

    Statement uses: Exists, Real, LT.lt, OfNat.ofNat, Filter.Eventually, Nat, Finset, Not, Membership.mem, Eq, Finset.card, Finset.sum, Real.cos, HMul.hMul, Neg.neg, Real.exp, Real.sqrt, Real.log, Filter.atTop

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

    26 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_510.variants.ruzsa :
    ∃ (c : ℝ) (hc : 0 < c),
      ∀ᶠ N in atTop, ∀ (A : Finset ℕ), 0 ∉ A → #A = N →
      ∃ θ, ∑ n ∈ A, cos (n * θ) < - exp (c * sqrt (log N)) := by
…

    Mentions: c

  3. theorem Erdos510.erdos_510.variants.bedert Bedert [Be25c] proved an upper bound of $-c N^{1/7}$ sorry line 65 source

    Source documentation

    Bedert [Be25c] proved an upper bound of $-c N^{1/7}$.

    depends on sorry what this means

    Statement uses: Exists, Real, LT.lt, OfNat.ofNat, Filter.Eventually, Nat, Finset, Not, Membership.mem, Eq, Finset.card, Finset.sum, Real.cos, HMul.hMul, Neg.neg, HPow.hPow, HDiv.hDiv, Filter.atTop

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

    46 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_510.variants.bedert :
    ∃ (c : ℝ) (hc : 0 < c),
      ∀ᶠ N in atTop, ∀ (A : Finset ℕ), 0 ∉ A → #A = N →
      ∃ θ, ∑ n ∈ A, cos (n * θ) < - c * N ^ (1 / 7 : ℝ) := by
…

    Mentions: c