Large sum-free subsets

DefinitionSum-free sets of natural numbers#✓fully proved

A finite set \(S\) of natural numbers is sum-free if \(x + y \notin S\) for all \(x, y \in S\), where \(x = y\) is allowed.

def IsSumFree (s : Finset ℕ) : Prop :=
  ∀ x ∈ s, ∀ y ∈ s, x + y ∉ s

Sources

• [GREEN-001].

Used by 2

Used byGreen's Problem 1 on large sum-free subsets · Number of maximal sum-free subsets of \(\{1, \dots, n\}\)

DefinitionGreen's Problem 1 on large sum-free subsets#✓fully proved

The statement that there is a function \(\omega\) from the natural numbers to the real numbers with \(\omega(n) \to \infty\) as \(n \to \infty\) such that every finite set \(A\) of positive integers contains a sum-free subset \(B \subseteq A\) with \(|B| \ge |A|/3 + \omega(|A|)\).

def conjecture : Prop :=
  ∃ ω : ℕ → ℝ, Filter.Tendsto ω Filter.atTop Filter.atTop ∧
    ∀ (A : Finset ℕ), (∀ a ∈ A, 0 < a) →
      ∃ B : Finset ℕ, B ⊆ A ∧ IsSumFree B ∧
        (A.card : ℝ) / 3 + ω (A.card) ≤ (B.card : ℝ)

Sources

• Ben Green, Problem 1 [GREEN-001].

Uses 1 · Used by 1

Statement usesSum-free sets of natural numbers

Used byBedert's theorem on large sum-free subsets

TheoremBedert's theorem on large sum-free subsets#●ready to prove

There is a function \(\omega\) from the natural numbers to the real numbers with \(\omega(n) \to \infty\) as \(n \to \infty\) such that every finite set \(A\) of positive integers contains a subset \(B \subseteq A\) with \(x + y \notin B\) for all \(x, y \in B\) (a sum-free subset) and \(|B| \ge |A|/3 + \omega(|A|)\).

Bedert proves more: every \(n\)-element set of integers contains a sum-free subset of size at least \(n/3 + c \log \log n\) for an absolute constant \(c > 0\). This answers Green's Problem 1.

public theorem_wanted conjecture_holds : conjecture

Sources

• Benjamin Bedert, Large sum-free subsets of sets of integers via L¹-estimates for trigonometric series, arXiv:2502.08624v1, https://arxiv.org/abs/2502.08624v1.

Uses 1

Statement usesGreen's Problem 1 on large sum-free subsets

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.