Dissociated subsets of real sets: the greedy bound (Erdős Problem 963)

f n is the largest k such that every set of n reals has a dissociated subset with at least k elements (definition copied verbatim from formal-conjectures). The greedy algorithm gives Nat.log 3 n ≤ f n: the elements that spoil a dissociated set B lie in its {-1, 0, 1}-span, of size at most 3 ^ #B.

Main results

• Erdos963.erdos_963.variants.greedy: Nat.log 3 n ≤ f n (Erdős 1965; formal-conjectures erdos_963.variants.greedy)
• Erdos963.card_span_le: the {-1,0,1}-span of B has at most 3^#B elements
• Erdos963.addDissociated_insert: B dissociated and x ∉ span B ⇒ insert x B dissociated
• Erdos963.exists_dissociated: 3^j ≤ #A ⇒ A has a dissociated subset with j elements

References

• P. Erdős, «Extremal problems in number theory», Proc. Sympos. Pure Math. VIII (1965) 181–189, p. 188.
• erdosproblems.com/963; statement and definition copied verbatim from google-deepmind/formal-conjectures, FormalConjectures/ErdosProblems/963.lean.

noncomputable def Erdos963.f (n : ℕ) : ℕ

$f(n)$ is the largest $k$ such that every set $A\subset\mathbb{R}$ with $n$ elements has a dissociated subset with at least $k$ elements. The set of such $k$ contains $0$ (take the empty subset) and is bounded by $n$, so sSup is a true maximum. The set $A$ may contain $0$, which can never belong to a dissociated set. For $n = 0$ the value is $0$.

Equations

• Erdos963.f n = sSup {k : ℕ | ∀ (A : Finset ℝ), A.card = n → ∃ B ⊆ A, k ≤ B.card ∧ AddDissociated ↑B}

theorem Erdos963.le_f {n k : ℕ} (h : ∀ (A : Finset ℝ), A.card = n → ∃ B ⊆ A, k ≤ B.card ∧ AddDissociated ↑B) : k ≤ f n

If every set of n reals has a dissociated subset with at least k elements, then $k \leq f(n)$.

noncomputable def Erdos963.span (B : Finset ℝ) : Finset ℝ

The {-1, 0, 1}-span of a finset of reals.

Equations

• Erdos963.span B = Finset.image (fun (ε : ↥B → ℤ) => ∑ b : ↥B, ↑(ε b) * ↑b) (Fintype.piFinset fun (x : ↥B) => {-1, 0, 1})

theorem Erdos963.card_span_le (B : Finset ℝ) : (span B).card ≤ 3 ^ B.card

theorem Erdos963.mem_span_of {B : Finset ℝ} (ε : ℝ → ℤ) (hε : ∀ (b : ℝ), ε b = -1 ∨ ε b = 0 ∨ ε b = 1) : ∑ b ∈ B, ↑(ε b) * b ∈ span B

theorem Erdos963.subset_span (B : Finset ℝ) : B ⊆ span B

theorem Erdos963.sub_mem_span {B t u : Finset ℝ} (ht : t ⊆ B) (hu : u ⊆ B) : ∑ a ∈ u, a - ∑ a ∈ t, a ∈ span B

Difference of two subset sums lies in the span.

theorem Erdos963.addDissociated_insert {B : Finset ℝ} {x : ℝ} (hB : AddDissociated ↑B) (hx : x ∉ span B) : AddDissociated ↑(insert x B)

Key step: adding an element outside the span keeps a set dissociated.

theorem Erdos963.exists_dissociated (A : Finset ℝ) (j : ℕ) : 3 ^ j ≤ A.card → ∃ B ⊆ A, B.card = j ∧ AddDissociated ↑B

Greedy construction: if 3 ^ j ≤ #A there is a dissociated B ⊆ A with #B = j.

theorem Erdos963.erdos_963.variants.greedy (n : ℕ) : Nat.log 3 n ≤ f n

Erdős noted that the greedy algorithm showed $f(n)\geq \lfloor \log_3 n\rfloor$ [Er65, p. 188].