Erdős Problem 12

Reference: erdosproblems.com/12

@[reducible, inline]

abbrev Erdos12.IsGood (A : Set ℕ) : Prop

A set A is "good" if it is infinite and there are no distinct a,b,c in A such that a ∣ (b+c) and b > a, c > a.

Equations

• Erdos12.IsGood A = (A.Infinite ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, a ∣ b + c → a < b → a < c → b = c)

theorem Erdos12.isGood_example : IsGood {x : ℕ | ∃ (p : ℕ) (_ : p ≡ 3 [MOD 4]) (_ : Nat.Prime p), p ^ 2 = x}

The set of $p ^ 2$ where $p \cong 3 \mod 4$ is prime is an example of a good set.

theorem Erdos12.erdos_12.parts.i : (∃ (A : Set ℕ), IsGood A ∧ 0 < Filter.liminf (fun (N : ℕ) => ↑(Erdos12.Set.bdd✝ A N).card / √↑N) Filter.atTop) ↔ sorry

Let $A$ be an infinite set such that there are no distinct $a,b,c \in A$ such that $a \mid (b+c)$ and $b,c > a$. Is there such an $A$ with $\liminf \frac{|A \cap \{1, \dotsc, N\}|}{N^{1/2}} > 0$ ?

theorem Erdos12.erdos_12.parts.ii : (∃ c > 0, ∀ (A : Set ℕ), IsGood A → {N : ℕ | ↑(Erdos12.Set.bdd✝ A N).card < ↑N ^ (1 - c)}.Infinite) ↔ sorry

Let $A$ be an infinite set such that there are no distinct $a,b,c \in A$ such that $a \mid (b+c)$ and $b,c > a$. Does there exist some absolute constant $c > 0$ such that there are always infinitely many $N$ with $|A \cap \{1, \dotsc, N\}| < N^{1−c}$?

theorem Erdos12.erdos_12.parts.iii : (∀ (A : Set ℕ), IsGood A → Summable fun (n : ↑A) => 1 / ↑↑n) ↔ sorry

Let $A$ be an infinite set such that there are no distinct $a,b,c \in A$ such that $a \mid (b+c)$ and $b,c > a$. Is it true that $∑_{n \in A} \frac{1}{n} < \infty$?

theorem Erdos12.erdos_12.variants.erdos_sarkozy_density_0 (A : Set ℕ) (hA : IsGood A) : A.HasDensity 0

Erdős and Sárközy proved that such an $A$ must have density 0. [ErSa70] Erd\H os, P. and Sárk"ozi, A., On the divisibility properties of sequences of integers. Proc. London Math. Soc. (3) (1970), 97-101

theorem Erdos12.erdos_12.variants.erdos_sarkozy (f : ℕ → ℕ) (hf : Filter.Tendsto f Filter.atTop Filter.atTop) : ∃ (A : Set ℕ), IsGood A ∧ {N : ℕ | ↑N / ↑(f N) < ↑(Erdos12.Set.bdd✝ A N).card}.Infinite

Given any function $f(x)\to \infty$ as $x\to \infty$ there exists a set $A$ with the property that there are no distinct $a,b,c \in A$ such that $a \mid (b+c)$ and $b,c > a$, such that there are infinitely many $N$ such that [\lvert A\cap{1,\ldots,N}\rvert > \frac{N}{f(N)}.

theorem Erdos12.erdos_12.variants.example (A : Set ℕ) (hA : A = {x : ℕ | ∃ (p : ℕ) (_ : Nat.Prime p) (_ : p ≡ 3 [MOD 4]), p ^ 2 = x}) : IsGood A ∧ 0 < Filter.liminf (fun (N : ℕ) => ↑(Erdos12.Set.bdd✝ A N).card * Real.log ↑N / √↑N) Filter.atTop

An example of an $A$ with the property that there are no distinct $a,b,c \in A$ such that $a \mid (b+c)$ and $b,c > a$ and such that [\liminf \frac{\lvert A\cap{1,\ldots,N}\rvert}{N^{1/2}}\log N > 0] is given by the set of $p^2$, where $p\equiv 3\pmod{4}$ is prime.

theorem Erdos12.erdos_12.variants.schoen (A : Set ℕ) (hA : IsGood A) (hA' : A.Pairwise Nat.Coprime) : (fun (N : ℕ) => ↑(Erdos12.Set.bdd✝ A N).card) =O[Filter.atTop] fun (N : ℕ) => ↑N ^ (2 / 3)

Let $A$ be a set of natural numbers with the property that there are no distinct $a,b,c \in A$ such that $a \mid (b+c)$ and $b,c > a$. If all elements in $A$ are pairwise coprime then [\lvert A\cap{1,\ldots,N}\rvert \ll N^{2/3}]

theorem Erdos12.erdos_12.variants.baier (A : Set ℕ) (hA : IsGood A) (hA' : A.Pairwise Nat.Coprime) : (fun (N : ℕ) => ↑(Erdos12.Set.bdd✝ A N).card) =O[Filter.atTop] fun (N : ℕ) => ↑N ^ (2 / 3) / Real.log ↑N

Let $A$ be a set of natural numbers with the property that there are no distinct $a,b,c \in A$ such that $a \mid (b+c)$ and $b,c > a$. If all elements in $A$ are pairwise coprime then [\lvert A\cap{1,\ldots,N}\rvert \ll N^{2/3}/\log N]