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

Reference: erdosproblems.com/319

Imports (1)
  1. theorem Erdos319.erdos_319 What is the size of the largest sorry line 45 source

    Source documentation

    What is the size of the largest $A\subseteq\{1, \dots, N\}$ such that there is a function $\delta : A \to \{-1, 1\}$ such that $$ \sum_{n\in A} \frac{\delta n}{n} = 0 $$ and $$ \sum_{n\in A'}\frac{\delta n}{n} \neq 0 $$ for all non-empty $A'\subsetneq A$.

    depends on sorry what this means

    Statement uses: Nat, IsGreatest, Set.ofPred, Exists, Finset, LE.le, Finset.Icc, OfNat.ofNat, Units, Int, And, Eq, Rat, Finset.sum, HDiv.hDiv, LT.lt, Finset.Nonempty, Ne, Finset.card, sorryAx and 1 more

    Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_319 (N : ℕ) : IsGreatest
    { #A | (A) (_ : A ⊆ Finset.Icc 1 N)
      (_ : ∃ δ : ℕ → ℤˣ, ∑ n ∈ A, (δ n : ℚ) / n = 0 ∧
        ∀ A' ⊂ A, A'.Nonempty → ∑ n ∈ A', (δ n : ℚ) / n ≠ 0) }
    answer(sorry) := by
…
  2. theorem Erdos319.erdos_319.variants.isTheta Documented declaration: isTheta sorry line 69 source

    Source documentation

    Let $c(N)$ be the size of the largest $A\subseteq\{1, \dots, N\}$ such that there is a function $\delta : A \to \{-1, 1\}$ such that $$ \sum_{n\in A} \frac{\delta n}{n} = 0 $$ and $$ \sum_{n\in A'}\frac{\delta n}{n} \neq 0 $$ for all non-empty $A'\subsetneq A$. What is $\Theta(c(N))$?

    Trivially $c(N) \leq N$, and erdos_319.variants.lb gives $c(N) \geq (1 - \frac{1}{e} + o(1))N$, so $c(N) = \Theta(N)$.

    depends on sorry what this means

    Statement uses: Nat, Real, IsGreatest, Set.ofPred, Exists, Finset, LE.le, Finset.Icc, OfNat.ofNat, Units, Int, And, Eq, Rat, Finset.sum, HDiv.hDiv, LT.lt, Finset.Nonempty, Ne, Finset.card and 2 more

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

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_319.variants.isTheta (N : ℕ) (c : ℕ → ℝ)
    (h : ∀ N, IsGreatest
    { (#A : ℝ) | (A) (_ : A ⊆ Finset.Icc 1 N)
      (_ : ∃ δ : ℕ → ℤˣ, ∑ n ∈ A, (δ n : ℚ) / n = 0 ∧
        ∀ A' ⊂ A, A'.Nonempty → ∑ n ∈ A', (δ n : ℚ) / n ≠ 0) } (c N)) :
    c =Θ[atTop] (answer(fun N ↦ (N : ℝ)) : ℕ → ℝ) := by
…

    Mentions: c

  3. theorem Erdos319.erdos_319.variants.lb Adenwalla has observed that a lower bound (on the maximum size of $A$) of $$ |A| \geq (1 - \frac{1}{e} + o(1))N $$ follows from the main result of Croot [Cr01] sorry line 87 source

    Source documentation

    Adenwalla has observed that a lower bound (on the maximum size of $A$) of $$ |A| \geq (1 - \frac{1}{e} + o(1))N $$ follows from the main result of Croot [Cr01].

    [Cr01] Croot, III, Ernest S., On unit fractions with denominators in short intervals. Acta Arith. (2001), 99-114.

    depends on sorry what this means

    Statement uses: Exists, Nat, Real, And, Asymptotics.IsLittleO, Filter.atTop, OfNat.ofNat, Filter.Eventually, LE.le, HMul.hMul, HAdd.hAdd, HSub.hSub, HDiv.hDiv, Real.exp, SupSet.sSup, Set.ofPred, Finset, Finset.Icc, Units, Int and 7 more

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

    64 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_319.variants.lb : ∃ (o : ℕ → ℝ), (o =o[atTop] (1 : ℕ → ℝ)) ∧
    ∀ᶠ N in atTop, (1 - 1 / rexp 1 + o N) * N ≤ sSup { (#A : ℝ) | (A) (_ : A ⊆ Finset.Icc 1 N)
      (_ : ∃ δ : ℕ → ℤˣ, ∑ n ∈ A, (δ n : ℚ) / n = 0 ∧
        ∀ A' ⊂ A, A'.Nonempty → ∑ n ∈ A', (δ n : ℚ) / n ≠ 0) } := by
…