FormalConjectures/ErdosProblems/786.lean

GitHub source file

9 declarations, 3 contain sorry, 0 declared as axioms

1. def Erdos786.Set.IsMulCardSet Nat.IsMulCardSet A means that A is a set of natural numbers that satisfies the property that $a_1\cdots a_r = b_1\cdots b_s$ with $a_i, b_j\in A$ can only hold when $r = s$ line 44 source

   Source documentation

   Nat.IsMulCardSet A means that A is a set of natural numbers that satisfies the property that $a_1\cdots a_r = b_1\cdots b_s$ with $a_i, b_j\in A$ can only hold when $r = s$.

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

   Statement uses: CommMonoid, Set

   Proof uses: Finset, LE.le, Eq, Finset.prod, id, Nat, Finset.card

   3 instances, coercions and auxiliary constants left out.

   def Set.IsMulCardSet {α : Type*} [CommMonoid α] (A : Set α) :=
   …

2. theorem Erdos786.erdos_786.parts.i Let $\epsilon > 0$ sorry line 54 source

   Source documentation

   Let $\epsilon > 0$. Is there some set $A\subset\mathbb{N}$ of density $> 1 - \epsilon$ such that $a_1\cdots a_r = b_1\cdots b_s$ with $a_i, b_j\in A$ can only hold when $r = s$?

   depends on sorry what this means

   Statement uses: Iff, True, Real, GT.gt, OfNat.ofNat, LE.le, Exists, Set, Nat, And, Not, Membership.mem, LT.lt, HSub.hSub, Set.HasDensity, Set.univ, Erdos786.Set.IsMulCardSet

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

   30 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_786.parts.i : answer(sorry) ↔ ∀ ε > 0, ε ≤ 1 →
       ∃ (A : Set ℕ) (δ : ℝ), 0 ∉ A ∧ 1 - ε < δ ∧ A.HasDensity δ ∧ A.IsMulCardSet := by
   …

3. theorem Erdos786.erdos_786.parts.ii Is there some set $A\subset\{1, ..., N\}$ of size $\geq (1 - o(1))N$ such that $a_1\cdots a_r = b_1\cdots b_s$ with $a_i, b_j\in A$ can only hold when $r = s$? sorry line 64 source

   Source documentation

   Is there some set $A\subset\{1, ..., N\}$ of size $\geq (1 - o(1))N$ such that $a_1\cdots a_r = b_1\cdots b_s$ with $a_i, b_j\in A$ can only hold when $r = s$?

   depends on sorry what this means

   Statement uses: Iff, True, Exists, Nat, Set, Real, Asymptotics.IsLittleO, Filter.atTop, OfNat.ofNat, And, LE.le, Set.Icc, HAdd.hAdd, HMul.hMul, HSub.hSub, Set.ncard, Erdos786.Set.IsMulCardSet

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

   34 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_786.parts.ii : answer(sorry) ↔
       ∃ (A : ℕ → Set ℕ) (f : ℕ → ℝ) (_ : f =o[atTop] (1 : ℕ → ℝ)),
       ∀ N, A N ⊆ Set.Icc 1 (N + 1) ∧ (1 - f N) * N ≤ (A N).ncard ∧ (A N).IsMulCardSet := by
   …

4. theorem Erdos786.erdos_786.parts.i.example An example of such a set with density $\frac 1 4$ is given by the integers $\equiv 2\pmod{4}$ line 73 source

   Source documentation

   An example of such a set with density $\frac 1 4$ is given by the integers $\equiv 2\pmod{4}$

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

   Statement uses: Set, Nat, Eq, Set.ofPred, HMod.hMod, OfNat.ofNat, And, Set.HasDensity, HDiv.hDiv, Real, Set.univ, Erdos786.Set.IsMulCardSet

   Proof uses: And.intro, Finset.card, Finset.filter, Finset.range, HAdd.hAdd, Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, Finset, EmptyCollection.emptyCollection, Finset.filter_empty, congrFun', zero_add, eq_self, Eq.mpr, Insert.insert, id and 194 more

   264 instances, coercions and auxiliary constants left out.

   Tactic trace: 81 steps

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

   theorem erdos_786.parts.i.example (A : Set ℕ) (hA : A = { n | n % 4 = 2 }) :
       A.HasDensity (1 / 4) ∧ A.IsMulCardSet := by
   …

5. def Erdos786.consecutivePrimesFrom consecutivePrimesFrom p k gives the set of k + 1 consecutive primes that are at least p in size line 147 source

   Source documentation

   consecutivePrimesFrom p k gives the set of k + 1 consecutive primes that are at least p in size. If p is prime then this is the set of k + 1 consecutive primes p, p_1, ..., p_k

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

   Statement uses: Nat, Finset

   Proof uses: Finset.image, Nat.nth, And, Nat.Prime, LE.le, Finset.range, HAdd.hAdd, OfNat.ofNat

   5 instances, coercions and auxiliary constants left out.

   noncomputable def consecutivePrimesFrom (p : ℕ) (k : ℕ) : Finset ℕ :=
   …

6. theorem Erdos786.nth_zero line 151 source

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

   Statement uses: Nat, Nat.Prime, Eq, Nat.nth, And, LE.le, OfNat.ofNat

   Proof uses: Eq.mpr, InfSet.sInf, Set.ofPred, id, congrFun', congrArg, Nat.nth_zero, IsLeast.csInf_eq, of_eq_true, Membership.mem, Set, lowerBounds, Eq.trans, True, congr, eq_true, and_self, forall_congr, implies_congr_ctx, Eq.refl and 1 more

   18 instances, coercions and auxiliary constants left out.

   Tactic trace: 2 steps

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

7. lemma Erdos786.consecutivePrimesFrom_zero line 157 source

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

   Statement uses: Nat, Nat.Prime, Eq, Finset, Erdos786.consecutivePrimesFrom, OfNat.ofNat, Singleton.singleton

   Proof uses: Eq.mpr, Nat.nth, And, LE.le, id, Eq.trans, congrFun', congrArg, Finset.image, Finset.range, HAdd.hAdd, zero_add, Finset.image_singleton, Erdos786.nth_zero

   11 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

8. lemma Erdos786.consecutivePrimesFrom_two_one line 161 source

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

   Statement uses: Eq, Finset, Nat, Erdos786.consecutivePrimesFrom, OfNat.ofNat, Insert.insert, Singleton.singleton

   Proof uses: Nat.nth, And, Nat.Prime, LE.le, Nat.nth_count, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Finset.ext, Eq.mpr, Iff, Membership.mem, Exists, LT.lt, HAdd.hAdd, Or, congr and 14 more

   28 instances, coercions and auxiliary constants left out.

   Tactic trace: 17 steps

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

9. theorem Erdos786.erdos_786.parts.i.selfridge Let $\epsilon > 0$ be given sorry line 187 source

   Source documentation

   Let $\epsilon > 0$ be given. Then, for a sufficiently large prime p, take the sequence of consecutive primes $p_1 < \cdots < p_k$ such that $$ \sum_{i=1}^k \frac{1}{p_i} < 1 < \sum_{i=1}^{k + 1} \frac{1}{p_i}, $$ and let $A$ be the set of all naturals divisible by exactly one of $p_1, ..., p_k$ (with multiplicity $1$). Then $A$ has density $> \frac{1}{e} - \epsilon$ and has the property that $a_1\cdots a_r = b_1\cdots b_s$ with $a_i, b_j\in A$ can only hold when $r = s$.

   depends on sorry what this means

   Statement uses: Real, And, LT.lt, OfNat.ofNat, HDiv.hDiv, Real.exp, Filter.Eventually, Nat, Nat.Prime, Exists, Finset.sum, Erdos786.consecutivePrimesFrom, HAdd.hAdd, HSub.hSub, Set.HasDensity, Set.ofPred, Eq, Finsupp, Nat.factorization, Set.univ and 2 more

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

   52 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_786.parts.i.selfridge (ε : ℝ) (hε : 0 < ε ∧ ε < 1 / rexp 1) :
       ∀ᶠ (p : ℕ) in atTop, p.Prime → ∃ k,
         ∑ q ∈ consecutivePrimesFrom p k, (1 : ℝ) / q < 1 ∧
           1 < ∑ q ∈ consecutivePrimesFrom p (k + 1), (1 : ℝ) / q ∧
             letI A := { n | ∑ q ∈ consecutivePrimesFrom p k, (n : ℕ).factorization q = 1 }
   …

   Mentions: Erdos786.consecutivePrimesFrom