Erdős Problem 786

Reference: erdosproblems.com/786

def Erdos786.Set.IsMulCardSet {α : Type u_1} [CommMonoid α] (A : Set α) : Prop

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$.

Equations

• Erdos786.Set.IsMulCardSet A = ∀ (a b : Finset α), ↑a ⊆ A → ↑b ⊆ A → a.prod id = b.prod id → a.card = b.card

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

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$?

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

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$?

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

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

noncomputable def Erdos786.consecutivePrimesFrom (p k : ℕ) : Finset ℕ

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

Equations

• Erdos786.consecutivePrimesFrom p k = Finset.image (Nat.nth fun (q : ℕ) => Nat.Prime q ∧ p ≤ q) (Finset.range (k + 1))

theorem Erdos786.nth_zero {p : ℕ} (hp : Nat.Prime p) : Nat.nth (fun (q : ℕ) => Nat.Prime q ∧ p ≤ q) 0 = p

theorem Erdos786.consecutivePrimesFrom_zero {p : ℕ} (hp : Nat.Prime p) : consecutivePrimesFrom p 0 = {p}

theorem Erdos786.consecutivePrimesFrom_two_one : consecutivePrimesFrom 2 1 = {2, 3}

theorem Erdos786.erdos_786.parts.i.selfridge (ε : ℝ) (hε : 0 < ε ∧ ε < 1 / Real.exp 1) : ∀ᶠ (p : ℕ) in Filter.atTop, Nat.Prime p → ∃ (k : ℕ), ∑ q ∈ consecutivePrimesFrom p k, 1 / ↑q < 1 ∧ 1 < ∑ q ∈ consecutivePrimesFrom p (k + 1), 1 / ↑q ∧ {n : ℕ | ∑ q ∈ consecutivePrimesFrom p k, n.factorization q = 1}.HasDensity (1 / Real.exp 1 - ε) ∧ Set.IsMulCardSet {n : ℕ | ∑ q ∈ consecutivePrimesFrom p k, n.factorization q = 1}

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$.