FormalConjectures/ErdosProblems/358.lean

GitHub source file

11 declarations, 5 contain sorry, 0 declared as axioms

1. def Erdos358.intervalRepresentations Let $a$ be an infinite sequence of integers line 38 source

   Source comment

   Let $a$ be an infinite sequence of integers. `intervalRepresentations A n` is the set of solutions to $$n=\sum_{u\leq i\leq v}a_i.$$ where `u` and `v` are positive integers.

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

   Statement uses: Nat, Set, Prod

   Proof uses: Set.ofPred, Erdos358.intervalRepresentations.match_1, And, LT.lt, OfNat.ofNat, Eq, Finset.sum, Finset.Icc

   5 instances, coercions and auxiliary constants left out.

   def intervalRepresentations (A : ℕ → ℕ) (n : ℕ) : Set (ℕ × ℕ) :=
   …

2. def Erdos358.f Let $a$ be an infinite sequence of integers line 45 source

   Source comment

   Let $a$ be an infinite sequence of integers. Let $f(n)$ count the number of solutions to $$n=\sum_{u\leq i\leq v}a_i.$$

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

   Statement uses: Nat

   Proof uses: Nat.card, Prod, Erdos358.intervalRepresentations

   1 instances, coercions and auxiliary constants left out.

   noncomputable def f (A : ℕ → ℕ) (n : ℕ) : ℕ :=
   …

3. def Erdos358.intervalRepresentationsNonTrivial Let $a$ be an infinite sequence of integers line 52 source

   Source comment

   Let $a$ be an infinite sequence of integers. `intervalRepresentationsNonTrivial A n` is the set of solutions to $$n=\sum_{u\leq i\leq v}a_i$$ such that the sum has at least two terms.

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

   Statement uses: Nat, Set, Prod

   Proof uses: Set.ofPred, Erdos358.intervalRepresentations.match_1, And, LT.lt, OfNat.ofNat, Eq, Finset.sum, Finset.Icc

   5 instances, coercions and auxiliary constants left out.

   def intervalRepresentationsNonTrivial (A : ℕ → ℕ) (n : ℕ) : Set (ℕ × ℕ) :=
   …

4. def Erdos358.g Let $a$ be an infinite sequence of integers line 59 source

   Source comment

   Let $a$ be an infinite sequence of integers. Let $g(n)$ count the number of solutions to $$n=\sum_{u\leq i\leq v}a_i.$$ such that the sum has at least two terms.

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

   Statement uses: Nat

   Proof uses: Nat.card, Prod, Erdos358.intervalRepresentationsNonTrivial

   1 instances, coercions and auxiliary constants left out.

   noncomputable def g (A : ℕ → ℕ) (n : ℕ) : ℕ :=
   …

5. theorem Erdos358.f_id When $A_n = n$, the function $f$ defined above counts the number of odd divisors of $n$ sorry line 66 source

   Source documentation

   When $A_n = n$, the function $f$ defined above counts the number of odd divisors of $n$.

   depends on sorry what this means

   Statement uses: Eq, Nat, Erdos358.f, id, Finset.card, Finset.filter, Odd, Nat.divisors

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

   5 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem f_id : f id = fun n ↦ #{d ∈ n.divisors | Odd d} := by
   …

   Mentions: Erdos358.f

6. theorem Erdos358.erdos_358.parts.i Let $A=\{a_1 < \cdots\}$ be an infinite sequence of integers sorry line 77 source

   Source documentation

   Let $A=\{a_1 < \cdots\}$ be an infinite sequence of integers. Let $f(n)$ count the number of solutions to $$n=\sum_{u\leq i\leq v}a_i.$$ Is there such an $A$ for which $f(n)\to \infty$ as $n\to \infty$?

   Tao [Ta26] constructed such a sequence with $f(n) \gg \log n$ for all sufficiently large $n$.

   depends on sorry what this means

   Statement uses: Iff, True, Exists, Nat, And, StrictMono, Filter.Tendsto, Erdos358.f, Filter.atTop

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

   3 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_358.parts.i :
       answer(True) ↔ ∃ A, StrictMono A ∧ atTop.Tendsto (f A) atTop := by
   …

   Mentions: Erdos358.f

7. theorem Erdos358.erdos_358.parts.ii Let $A=\{a_1 < \cdots\}$ be an infinite sequence of integers sorry line 89 source

   Source documentation

   Let $A=\{a_1 < \cdots\}$ be an infinite sequence of integers. Let $f(n)$ count the number of solutions to $$n=\sum_{u\leq i\leq v}a_i.$$ Is there an $A$ such that $f(n)\geq 2$ for all large $n$?

   This also follows from Tao's construction with $f(n) \gg \log n$ [Ta26].

   depends on sorry what this means

   Statement uses: Iff, True, Exists, Nat, And, StrictMono, Filter.Eventually, LE.le, OfNat.ofNat, Erdos358.f, Filter.atTop

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

   6 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_358.parts.ii :
       answer(True) ↔ ∃ A, StrictMono A ∧ ∀ᶠ n in atTop, 2 ≤ f A n := by
   …

   Mentions: Erdos358.f

8. theorem Erdos358.erdos_358.variants.prime_set When $A =\{a_1 < \cdots\}$ corresponds to the set of primes, it is conjectured that the $\limsup$ of the number of representations $$n=\sum_{u\leq i\leq v}a_i$$ is infinite sorry line 98 source

   Source documentation

   When $A =\{a_1 < \cdots\}$ corresponds to the set of primes, it is conjectured that the $\limsup$ of the number of representations $$n=\sum_{u\leq i\leq v}a_i$$ is infinite.

   depends on sorry what this means

   Statement uses: Eq, ENat, Filter.limsup, Nat, Erdos358.f, Nat.nth, Nat.Prime, Filter.atTop, Top.top

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

   17 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_358.variants.prime_set :
       atTop.limsup (fun n ↦ (f (Nat.nth Nat.Prime) n : ℕ∞)) = ⊤ := by
   …

   Mentions: Erdos358.f

9. theorem Erdos358.erdos_358.variants.prime_set_density_representation Documented declaration: prime_set_density_representation sorry line 107 source

   Source documentation

   When $A =\{a_1 < \cdots\}$ corresponds to the set of primes, it is conjectured that the set of numbers $n$ that have representations $$n=\sum_{u\leq i\leq v}a_i$$ has positive upper density.

   depends on sorry what this means

   Statement uses: LT.lt, Real, OfNat.ofNat, Set.upperDensity, Nat, Set.ofPred, Set.Nonempty, Prod, Erdos358.intervalRepresentations, Nat.nth, Nat.Prime, Set.univ

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

   15 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_358.variants.prime_set_density_representation :
       0 < {n : ℕ | intervalRepresentations (Nat.nth Nat.Prime) n |>.Nonempty}.upperDensity := by
   …

   Mentions: Erdos358.intervalRepresentations

10. theorem Erdos358.one_le_g_of_two_le_f Documented declaration: one_le_g_of_two_le_f line 117 source

    Source documentation

    If $A$ is strictly increasing then any $n > 0$ has at most one representation $$n=\sum_{u\leq i\leq v}a_i$$ with a single term, so discarding the single-term representations loses at most one solution.

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

    Statement uses: Nat, StrictMono, LT.lt, OfNat.ofNat, LE.le, Erdos358.f, Erdos358.g

    Proof uses: Set.Finite, Prod, Erdos358.intervalRepresentations, Set.Infinite, Or, Set.finite_or_infinite, Decidable.byContradiction, Classical.propDecidable, Not, Eq.mp, Nat.card, congrArg, Nat.card_eq_zero_of_infinite, Set.Infinite.to_subtype, Erdos358.f.eq_1, Set, Erdos358.intervalRepresentationsNonTrivial, Membership.mem, Prod.mk, id and 45 more

    35 instances, coercions and auxiliary constants left out.

    Tactic trace: 43 steps

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

    theorem one_le_g_of_two_le_f {A : ℕ → ℕ} (hA : StrictMono A) {n : ℕ} (hn : 0 < n)
        (hf : 2 ≤ f A n) : 1 ≤ g A n := by
    …

    Mentions: Erdos358.f, Erdos358.g

11. theorem Erdos358.erdos_358.variants.one_le In [ErGr80] Erdős and Graham further asked whether there is an $A$ with $f(n)\geq 1$ for all large $n$ line 168 source

    Source documentation

    In [ErGr80] Erdős and Graham further asked whether there is an $A$ with $f(n)\geq 1$ for all large $n$. Egami observed that this holds trivially for $a_n=n$, so they may have intended to count only those representations $$n=\sum_{u\leq i\leq v}a_i$$ that use at least two consecutive terms, which is what $g$ counts.

    This follows from Tao's construction [Ta26], which gives $f(n)\gg\log n$: see erdos_358.parts.ii and one_le_g_of_two_le_f.

    depends on sorry what this means

    Statement uses: Exists, Nat, And, StrictMono, Filter.Eventually, LE.le, OfNat.ofNat, Erdos358.g, Filter.atTop

    Proof uses: Erdos358.f, Iff.mp, True, Erdos358.erdos_358.parts.ii, trivial, Exists.intro, And.intro, Filter.mp_mem, Set.ofPred, LT.lt, Filter.eventually_gt_atTop, Membership.mem, Set, Filter.univ_mem', id, Erdos358.one_le_g_of_two_le_f

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

    theorem erdos_358.variants.one_le :
        ∃ A, StrictMono A ∧ ∀ᶠ n in atTop, 1 ≤ g A n := by
    …

    Mentions: Erdos358.g