Erdős Problem 789

In this problem, a function $h : \mathbb{N} \to\mathbb{N}$ is defined maximally by some 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 $\sqrt{n}$ and the best known lower bound is $(n\log(n))^{1/3}$ so we also provide these candidates as variants. Moreover, it suffices to show $O(h(n))$ and $O((n\log(n))^{1/3})$ respectively for each, so further variants are provided for those.

References:

• erdosproblems.com/789
• [Str66] Straus, E. G., On a problem in combinatorial number theory. J. Math. Sci. (1966), 77--80.
• [Er62c] Erdős, Pál, Some remarks on number theory. {III}. Mat. Lapok (1962), 28--38.
• [Ch74b] Choi, S. L. G., On an extremal problem in number theory. J. Number Theory (1974), 105--111.

def Erdos789.IsSubsetSumSeparatingCard (n m : ℕ) : Prop

Given a non-negative integer $n$, we say $m$ is a separating cardinality of subset sums if, for any set $A$ of $n$ integers, there is some $B\subseteq A$ of size $\geq m$ such that subset sums of $B$ can only ever coincide when the subsets have the same cardinality.

Equations

• Erdos789.IsSubsetSumSeparatingCard n m = ∀ (A : Finset ℤ), A.card = n → ∃ B ⊆ A, m ≤ B.card ∧ ∀ T ⊆ B, ∀ S ⊆ B, S.Nonempty → T.Nonempty → ∑ a ∈ T, a = ∑ b ∈ S, b → T.card = S.card

noncomputable def Erdos789.subsetSumThreshold (n : ℕ) : ℕ

The subset sum threshold $h(n)$, for each positive $n$, is the maximal separating cardinality of subset sums for $n$.

Equations

• Erdos789.subsetSumThreshold n = sSup {m : ℕ | Erdos789.IsSubsetSumSeparatingCard n m}

theorem Erdos789.erdos_789 : (fun (n : ℕ) => ↑(subsetSumThreshold n)) =Θ[Filter.atTop] sorry

Let $h(n)$ be maximal such that if $A\subseteq \mathbb{Z}$ with $\lvert A\rvert=n$ then there is $B\subseteq A$ with $\lvert B\rvert \geq h(n)$ such that if $a_1+\cdots+a_r=b_1+\cdots+b_s$ with $a_i,b_i\in B$ then $r=s$.

Estimate $h(n)$.

theorem Erdos789.erdos_789.variants.sq : (fun (n : ℕ) => ↑(subsetSumThreshold n)) =Θ[Filter.atTop] fun (n : ℕ) => √↑n

Let $h(n)$ be maximal such that if $A\subseteq \mathbb{Z}$ with $\lvert A\rvert=n$ then there is $B\subseteq A$ with $\lvert B\rvert \geq h(n)$ such that if $a_1+\cdots+a_r=b_1+\cdots+b_s$ with $a_i,b_i\in B$ then $r=s$.

Is $h(n) = \Theta(\sqrt{n})$?

theorem Erdos789.erdos_789.variants.isBigO_sq : (fun (n : ℕ) => ↑(subsetSumThreshold n)) =O[Filter.atTop] fun (n : ℕ) => √↑n

Straus [Str66] proved that $h(n) \ll \sqrt{n}$.

theorem Erdos789.erdos_789.variants.sq_isBigO : (fun (n : ℕ) => √↑n) =O[Filter.atTop] fun (n : ℕ) => ↑(subsetSumThreshold n)

By the solved variant erdos_789.variants.isBigO_sq, in order to prove erdos_789.variants.sq it suffices to show $\sqrt{n}=O(h(n))$.

theorem Erdos789.erdos_789.variants.cube_root_linearithmic : (fun (n : ℕ) => ↑(subsetSumThreshold n)) =Θ[Filter.atTop] fun (n : ℕ) => (↑n * Real.log ↑n) ^ (1 / 3)

Let $h(n)$ be maximal such that if $A\subseteq \mathbb{Z}$ with $\lvert A\rvert=n$ then there is $B\subseteq A$ with $\lvert B\rvert \geq h(n)$ such that if $a_1+\cdots+a_r=b_1+\cdots+b_s$ with $a_i,b_i\in B$ then $r=s$.

Is $h(n) = \Theta((n\log(n)))^{1/3})$?

theorem Erdos789.erdos_789.variants.cube_root_linearithmic_isBigO : (fun (n : ℕ) => (↑n * Real.log ↑n) ^ (1 / 3)) =O[Filter.atTop] fun (n : ℕ) => ↑(subsetSumThreshold n)

Erdős [Er62c] and Choi [Ch74b] proved that $(n\log(n))^{1/3}\ll h(n)$.

theorem Erdos789.erdos_789.variants.isBigO_cube_root_linearithmic : (fun (n : ℕ) => ↑(subsetSumThreshold n)) =O[Filter.atTop] fun (n : ℕ) => (↑n * Real.log ↑n) ^ (1 / 3)

By the solved variant erdos_789.variants.cube_root_linearithmic_isBigO, in order to prove erdos_789.variants.cube_root_linarithmic it suffices to show $h(n) = O((n\log(n))^{1/3})$.