Erdős Problem 786

Reference: erdosproblems.com/786

def 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

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

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

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 erdos_786.parts.ii : (∃ (A : ℕ → Set ℕ) (f : ℕ → ℝ) (_ : Filter.Tendsto f Filter.atTop (nhds 0)), ∀ (N : ℕ), A N ⊆ Set.Icc 1 (N + 1) ∧ (1 - f N) * ↑N ≤ ↑(A N).ncard ∧ (A N).IsMulCardSet) ↔ sorry

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 erdos_786.parts.i.example (A : Set ℕ) (hA : A = {n : ℕ | n % 4 = 2}) : A.HasDensity (1 / 4) ∧ A.IsMulCardSet

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

def consecutivePrimes {k : ℕ} (p : Fin k.succ → ℕ) : Prop

consecutivePrimes p asserts that p is a strictly increasing finite sequences of consecutive primes.

Equations

• consecutivePrimes p = ∀ (i : Fin k.succ), Nat.Prime (p i) ∧ StrictMono p ∧ ∀ i < k, ∀ m ∈ Set.Ioo (p ↑i) (p (↑i + 1)), ¬Nat.Prime m

theorem erdos_786.parts.i.selfridge (ε : ℝ) (hε : 0 < ε ∧ ε ≤ 1) : ∃ (k : ℕ), ∀ᶠ (p : Fin (k + 2) → ℕ) in Filter.atTop, consecutivePrimes p ∧ ∑ i ∈ Finset.filter (fun (x : Fin (k + 1 + 1)) => x < Fin.last (k + 1)) Finset.univ, 1 / ↑(p i) < 1 ∧ 1 < ∑ i : Fin (k + 2), 1 / ↑(p i) → {n : ℕ | ∃! i : ℕ, i < k ∧ p ↑i ∣ n}.HasDensity (1 / Real.exp 1 - ε) ∧ {n : ℕ | ∃! i : ℕ, i < k ∧ p ↑i ∣ n}.IsMulCardSet

Let $\epsilon > 0$ be given. Then, for a sequence of sufficiently large 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}, $$ the set $A$ of all naturals divisible by exactly one of $p_1, ..., p_k$ has density $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$.