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 $\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$.
Actions
Submit a Proof
Have a proof attempt? Submit it for zero-trust verification.
theorem erdos_786.parts.i.selfridge (ε : ℝ) (hε : 0 < ε ∧ ε ≤ 1) :
-- TODO(mercuris) : I think we want `k` to be allowed to vary somehow as well, but maybe the
-- exists is sufficient
∃ (k : ℕ),
-- Sufficient to take L^∞ norm to guarantee all primes are large, due to the consecutivePrimes
-- assertion
∀ᶠ (p : Fin (k + 2) → ℕ) in atTop, consecutivePrimes p ∧
∑ i ∈ Finset.univ.filter (· < Fin.last _), (1 : ℝ) / p i < 1 ∧
1 < ∑ i, (1 : ℝ) / p i →
{ n | ∃! (i : Fin (k + 2)), i < k → p i ∣ n }.HasDensity (1 / Real.exp 1 - ε) ∧
{ n | ∃! (i : Fin (k + 2)), i < k → p i ∣ n }.IsMulCardSet
