Erdős Problem 774

Reference: erdosproblems.com/774

def Set.IsDissociated (A : Set ℕ) : Prop

We call $A\subset \mathbb{N}$ dissociated if $\sum_{n\in X}n\neq \sum_{m\in Y}m$ for all finite $X,Y\subset A$ with $X\neq Y$.

Equations

• A.IsDissociated = Set.InjOn (fun (S : Finset ℕ) => ∑ n ∈ S, n) {S : Finset ℕ | ↑S ⊆ A}

def Set.IsProportionatelyDissociated (A : Set ℕ) : Prop

We call $A$ proportionately dissociated if every finite $B\subset A$ contains a dissociated set of size $\gg \lvert B\rvert$.

In other words, there is a (global) $c > 0$ such that every finite $B \subset A$ contains a dissociated set of size $\geq c|B|$.

Equations

• A.IsProportionatelyDissociated = ∃ c > 0, ∀ (B : Finset ℕ), ↑B ⊆ A → ∃ S ⊆ B, ↑S.card ≥ c * ↑B.card ∧ (↑S).IsDissociated

theorem Erdos774.erdos_774 : True ↔ ∀ (A : Set ℕ), A.Infinite → A.IsProportionatelyDissociated → ∃ (T : Set (Set ℕ)), (∀ S ∈ T, S.IsDissociated) ∧ T.Finite ∧ A = ⋃₀ T

Is every proportionately dissociated (infinite) set the union of a finite number of dissociated sets?