Erdős Problem 26

References:

• erdosproblems.com/26
• Te19 G. Tenenbaum, Some of Erdős' unconventional problems in number theory, thirty-four years later, arXiv:1908.00488 [math.NT] (2019)

def Erdos26.IsThick {ι : Type u_1} (A : ι → ℕ) : Prop

A sequence of naturals $(a_i)$ is thick if their sum of reciprocals diverges: $$ \sum_i \frac{1}{a_i} = \infty $$

Equations

• Erdos26.IsThick A = ¬Summable fun (i : ι) => 1 / ↑(A i)

theorem Erdos26.not_isThick_of_finite {ι : Type u_1} [Finite ι] (A : ι → ℕ) : ¬IsThick A

theorem Erdos26.not_isThick_of_geom_one_lt (r : ℕ) (hr : r > 1) : ¬IsThick fun (n : ℕ) => r ^ n

theorem Erdos26.isThick_const {ι : Type u_1} [Infinite ι] (r : ℕ) (h : r > 0) : IsThick fun (x : ι) => r

def Erdos26.MultiplesOf {ι : Type u_1} (A : ι → ℕ) : Set ℕ

The set of multiples of a sequence $(a_i)$ is $\{na_i | n \in \mathbb{N}, i\}$.

Equations

• Erdos26.MultiplesOf A = Set.range fun (x : ℕ × ι) => match x with | (n, i) => n * A i

theorem Erdos26.multiplesOf_eq_univ {ι : Type u_1} (A : ι → ℕ) (h : 1 ∈ Set.range A) : MultiplesOf A = Set.univ

def Erdos26.IsBehrend {ι : Type u_1} (A : ι → ℕ) : Prop

A sequence of naturals $(a_i)$ is Behrend if almost all integers are a multiple of some $a_i$. In other words, if the set of multiples has natural density $1$.

Equations

• Erdos26.IsBehrend A = (Erdos26.MultiplesOf A).HasDensity 1

def Erdos26.IsWeaklyBehrend {ι : Type u_1} (A : ι → ℕ) (ε : ℝ) : Prop

A sequence of naturals $(a_i)$ is weakly Behrend with respect to $\varepsilon \in \mathbb{R}$ if at least $1 - \varepsilon$ density of all numbers are a multiple of $A$.

Equations

• Erdos26.IsWeaklyBehrend A ε = (1 - ε ≤ (Erdos26.MultiplesOf A).lowerDensity)

theorem Erdos26.isBehrend_of_contains_one {ι : Type u_1} (A : ι → ℕ) (h : 1 ∈ Set.range A) : IsBehrend A

theorem Erdos26.isWeaklyBehrend_of_ge_one {ι : Type u_1} (A : ι → ℕ) {ε : ℝ} (hε : 1 ≤ ε) : IsWeaklyBehrend A ε

theorem Erdos26.not_isWeaklyBehrend_of_neg {ι : Type u_1} (A : ι → ℕ) {ε : ℝ} (hε : ε < 0) : ¬IsWeaklyBehrend A ε

theorem Erdos26.erdos_26 (A : ℕ → ℕ) (hA : StrictMono A) (h : IsThick A) : (∃ (k : ℕ), IsBehrend fun (x : ℕ) => A x + k) ↔ sorry

Let $A\subset\mathbb{N}$ be infinite such that $\sum_{a \in A} \frac{1}{a} = \infty$. Must there exist some $k\geq 1$ such that almost all integers have a divisor of the form $a+k$ for some $a\in A$?

theorem Erdos26.erdos_26.variants.rusza : ∃ (A : ℕ → ℕ), StrictMono A ∧ ¬IsThick A ∧ ∀ (k : ℕ), ¬IsBehrend fun (x : ℕ) => A x + k

If we allow for $\sum_{a\in A} \frac{1}{a} < \infty$ then Rusza has found a counter-example.

theorem Erdos26.erdos_26.variants.tenenbaum (A : ℕ → ℕ) (hA : StrictMono A) (h : IsThick A) : (∀ ε > 0, ∃ (k : ℕ), IsWeaklyBehrend (fun (x : ℕ) => A x + k) ε) ↔ sorry

Tenenbaum asked the weaker variant where for every $\epsilon>0$ there is some $k=k(\epsilon)$ such that at least $1-\epsilon$ density of all integers have a divisor of the form $a+k$ for some $a\in A$.