Erdős Problem #963

The question

erdos_963.parts.i. Let $f(n)$ be the maximal $k$ such that in any set $A\subset \mathbb{R}$ of size $n$ there is a subset $B\subseteq A$ of size $|B|\ge k$ which is dissociated that is, the sums ${\sum }_{b\in S}b$ are distinct for all $S\subseteq B$. Estimate $f(n)$ - in particular, is it true that $f(n)\ge \lfloor {\log }_{2}n\rfloor$?

This is the first part, a problem of Erdős [Er65, p. 188]. We read "estimate" as an asymptotic equivalence $f(n)\sim$ answer n. The order of magnitude $\log n$ is easy (see erdos_963.variants.greedy and the example $a_i=i$ in [Er65, p. 188]), so the question is the constant.

erdos_963.parts.ii. Let $f(n)$ be the maximal $k$ such that in any set $A\subset \mathbb{R}$ of size $n$ there is a subset $B\subseteq A$ of size $|B|\ge k$ which is dissociated that is, the sums ${\sum }_{b\in S}b$ are distinct for all $S\subseteq B$. Estimate $f(n)$ - in particular, is it true that $f(n)\ge \lfloor {\log }_{2}n\rfloor$?

This is the second part. Erdős [Er65, p. 188] asks whether the bound $\lfloor {\log }_{3}n\rfloor$ can be improved to $\lfloor {\log }_{2}n\rfloor$. We state it for all $n\ge 1$, with $\lfloor {\log }_{2}n\rfloor$ written as Nat.log 2 n.

As on the problem page, $A$ is any set of reals. [Er65] speaks of "given numbers" and uses the example $a_i=i$. Allowing negative numbers makes the question harder. A dissociated set never contains both $x$ and $-x$, and changing signs keeps a set dissociated. So the largest dissociated subsets of $A$ and of $\{|a|:a\in A,a\ne 0\}$ have the same size, and the sets $\{\pm a:a\in S\}$ (with $0$ added for odd $n$) show that $f(2m)=f(2m+1)$ is the least size of a largest dissociated subset of a set of $m$ positive reals. Hence this statement asks for $\lfloor {\log }_{2}m\rfloor +1$ for $m$ positive reals. The question for positive reals with $\lfloor {\log }_2|A|\rfloor$, one less, is erdos_963.variants.positive; it follows from this statement.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.ErdosProblems.«963» (2 statements).

theorem erdos_963.parts.i :
    (fun n : ℕ ↦ (f n : ℝ)) ~[atTop] erdos_963.parts.i.answer

theorem erdos_963.parts.ii : ∀ n : ℕ, 1 ≤ n → Nat.log 2 n ≤ f n

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already — check erdosproblems.com/963. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

Variants

• erdos_963.variants.positive — The second part for sets of positive reals, with ⌊log_2lvert Arvert⌋ as in [Er65, p.

References

• erdosproblems.com/963
• [Er65] Erdős, P., Extremal problems in number theory. Proc. Sympos. Pure Math., Vol. VIII (1965), 181-189. PDF

A set B of real numbers is dissociated if all sums over its finite subsets are distinct. This is AddDissociated in Mathlib.

Source and licence

Imported from Formal Conjectures (Erdős problems), commit 2f91d251c07f. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.