Erdős Problem 539

In this problem, a function $h : \mathbb{N} \to\mathbb{N}$ is defined maximally by a specified counting property.

The problem asks to estimate $h(n)$. This has been interpreted here as asking for $\Theta(h(n))$. The principal version includes answer(sorry) for an unknown function. On the other hand, the best known upper bound is $n^{2/3}$ and the best known lower bound is $\sqrt{n}$ so we also provide these candidates as variants. Moreover, it suffices to show $O(h(n))$ and $O(\sqrt{n})$ respectively for each, so further variants are provided for those.

In the source paper [Er73], Erdős also remarks that it should not be too difficult to determine $\lim_{n\to\infty}\log(h(n))/\log(n)$. This does not appear on the website, and it is not clear whether this remains open, but we include it here either way.

References:

• erdosproblems.com/539
• [GR99] Granville, A., & Roesler, F. (1999). The Set of Differences of a Given Set. The American Mathematical Monthly, 106(4), 338–344.
• [Er73] Erdős, P., Problems and results on combinatorial number theory. A survey of combinatorial theory (Proc. Internat. Sympos., Colorado State Univ., Fort Collins, Colo., 1971) (1973), 117-138.

def Erdos539.IsCofactorLowerBound (n m : ℕ) : Prop

We say that $m$ is a cofactor lower bound for a given $n$ if, for every set $A$ of $n$ non-negative integers, there are at least $m$ cofactors $a / (a, b)$, where $a, b\in A$.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Erdos539.cofactorThreshold (n : ℕ) : ℕ

The cofactor threshold $h(n)$, for every positive $n$, is the largest cofactor lower bound for $n$.

Equations

• Erdos539.cofactorThreshold n = sSup {m : ℕ | Erdos539.IsCofactorLowerBound n m}

theorem Erdos539.erdos_539 : (fun (n : ℕ) => ↑(cofactorThreshold n)) =Θ[Filter.atTop] sorry

Let $h(n)$ be maximal such that, for any set $A\subseteq \mathbb{N}$ of size $n$, the set$$\left{ \frac{a}{(a,b)}: a,b\in A\right}$$has size at least $h(n)$. Estimate $h(n)$.

theorem Erdos539.erdos_539.variants.sq : (fun (n : ℕ) => ↑(cofactorThreshold n)) =Θ[Filter.atTop] fun (n : ℕ) => √↑n

Let $h(n)$ be maximal such that, for any set $A\subseteq \mathbb{N}$ of size $n$, the set$$\left{ \frac{a}{(a,b)}: a,b\in A\right}$$has size at least $h(n)$. Is $h(n) = \Theta(\sqrt{n})$?

theorem Erdos539.erdos_539.variants.sq_isBigO : (fun (n : ℕ) => √↑n) =O[Filter.atTop] fun (n : ℕ) => ↑(cofactorThreshold n)

Erdős and Szemerédi proved that$$n^{1/2} \ll h(n)$$.

theorem Erdos539.erdos_539.variants.isBigO_sq : (fun (n : ℕ) => ↑(cofactorThreshold n)) =O[Filter.atTop] fun (n : ℕ) => √↑n

To prove erdos_539.variants.sq it suffices to show $$ h(n)\ll n^{1/2}$$.

theorem Erdos539.erdos_539.variants.sq_cube_root : (fun (n : ℕ) => ↑(cofactorThreshold n)) =Θ[Filter.atTop] fun (n : ℕ) => ↑n ^ (2 / 3)

Let $h(n)$ be maximal such that, for any set $A\subseteq \mathbb{N}$ of size $n$, the set$$\left{ \frac{a}{(a,b)}: a,b\in A\right}$$has size at least $h(n)$. Is $h(n) = \Theta(n^{2/3})$?

theorem Erdos539.erdos_539.variants.isBigO_sq_cube_root : (fun (n : ℕ) => ↑(cofactorThreshold n)) =O[Filter.atTop] fun (n : ℕ) => ↑n ^ (2 / 3)

Granville and Roesler [GR99] showed that $$h(n)\ll n^{2/3}$$.

theorem Erdos539.erdos_539.variants.sq_cube_root_isBigO : (fun (n : ℕ) => ↑n ^ (2 / 3)) =O[Filter.atTop] fun (n : ℕ) => ↑(cofactorThreshold n)

To prove erdos_539.variants.sq_cube_root it suffices to show $$n^{2/3}\ll h(n)$$.

theorem Erdos539.erdos_539.variants.limit : Filter.Tendsto (fun (n : ℕ) => Real.log ↑(cofactorThreshold n) / Real.log ↑n) Filter.atTop sorry

From [Er73]: The determination of $$ \lim_{n\to\infty}\frac{\log(h(n))}{\log(n)} $$ will perhaps be not too difficult.