Number of sum-free sets

DefinitionNumber of maximal sum-free subsets of \(\{1, \dots, n\}\)#✓fully proved

For a natural number \(n\), \(f_m(n)\) is the number of sets \(A \subseteq \{1, \dots, n\}\) that are sum-free, meaning \(x + y \notin A\) for all \(x, y \in A\) (including \(x = y\)), and maximal with this property: every sum-free set \(B\) with \(A \subseteq B \subseteq \{1, \dots, n\}\) equals \(A\).

noncomputable def maximalSumFreeCount (n : ℕ) : ℕ :=
  ((Finset.Icc 1 n).powerset.filter fun A =>
    IsSumFree A ∧ ∀ B ⊆ Finset.Icc 1 n, A ⊆ B → IsSumFree B → B = A).card

Uses 1 · Used by 1

Statement usesSum-free sets of natural numbers

Used byErdős Problem 877 on maximal sum-free sets

DefinitionErdős Problem 877 on maximal sum-free sets#✓fully proved

Let \(f_m(n)\) be the number of maximal sum-free subsets of \(\{1, \dots, n\}\). This is the statement, asked by Cameron and Erdős, that \(f_m(n) / 2^{n/2} \to 0\) as \(n \to \infty\), that is, \(f_m(n) = o(2^{n/2})\).

def maximalSumFreeCountSmall : Prop :=
  Filter.Tendsto (fun n : ℕ => (maximalSumFreeCount n : ℝ) / 2 ^ ((n : ℝ) / 2))
    Filter.atTop (nhds 0)

Uses 1 · Used by 1

Statement usesNumber of maximal sum-free subsets of \(\{1, \dots, n\}\)

Used byMaximal sum-free subsets of \(\{1, \dots, n\}\) number \(o(2^{n/2})\)

TheoremMaximal sum-free subsets of \(\{1, \dots, n\}\) number \(o(2^{n/2})\)#●ready to prove

Let \(f_m(n)\) be the number of maximal sum-free subsets of \(\{1, \dots, n\}\). Then \(f_m(n) / 2^{n/2} \to 0\) as \(n \to \infty\), that is, \(f_m(n) = o(2^{n/2})\).

public theorem_wanted maximalSumFreeCountSmall_holds : maximalSumFreeCountSmall

Sources

• T. F. Bloom, Erdős Problems, Problem #877, https://www.erdosproblems.com/877 (status PROVED); resolution: T. Łuczak and T. Schoen, On the number of maximal sum-free sets, Proc. Amer. Math. Soc. 129 (2001), 2205-2207, abstract: {1, 2, …, n} contains at most 2^{n/2 - 2^{-28} n} maximal sum-free subsets, provided n is large enough; erdosproblems.com/877: this resolves the question, and Balogh, Liu, Sharifzadeh and Treglown later proved f_m(n) = 2^{(1/4 + o(1)) n}, https://doi.org/10.1090/S0002-9939-00-05815-9.

Uses 1

Statement usesErdős Problem 877 on maximal sum-free sets

DefinitionNumber of sum-free subsets of \(\{1, \dots, n\}\)#✓fully proved

For a natural number \(n\), \(f(n)\) is the number of sets \(A \subseteq \{1, \dots, n\}\) that are sum-free, meaning that there are no \(a, b, c \in A\) with \(a = b + c\) (the case \(b = c\) included). The empty set is counted.

def sumFreeCount (n : ℕ) : ℕ :=
  ((Finset.Icc 1 n).powerset.filter fun A => ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, a ≠ b + c).card

Used by 1

Used byErdős Problem 748 on the number of sum-free sets

DefinitionErdős Problem 748 on the number of sum-free sets#✓fully proved

Let \(f(n)\) be the number of sum-free subsets of \(\{1, \dots, n\}\). This is the statement that \(\log_2 f(n) / n \to 1/2\) as \(n \to \infty\), that is, \(f(n) = 2^{(1 + o(1)) n / 2}\).

def sumFreeCountExponent : Prop :=
  Filter.Tendsto (fun n : ℕ => Real.logb 2 (sumFreeCount n) / n) Filter.atTop (nhds (1 / 2))

Uses 1 · Used by 1

Statement usesNumber of sum-free subsets of \(\{1, \dots, n\}\)

Used bySum-free subsets of \(\{1, \dots, n\}\) number \(2^{(1 + o(1)) n / 2}\)

TheoremSum-free subsets of \(\{1, \dots, n\}\) number \(2^{(1 + o(1)) n / 2}\)#●ready to prove

Let \(f(n)\) be the number of sum-free subsets of \(\{1, \dots, n\}\), that is, of sets \(A \subseteq \{1, \dots, n\}\) with no \(a, b, c \in A\) satisfying \(a = b + c\) (the case \(b = c\) included). Then \(\log_2 f(n) / n \to 1/2\) as \(n \to \infty\), that is, \(f(n) = 2^{(1 + o(1)) n / 2}\).

public theorem_wanted sumFreeCountExponent_holds : sumFreeCountExponent

Sources

• T. F. Bloom, Erdős Problems, Problem #748, https://www.erdosproblems.com/748 (status PROVED); resolution: B. Green, The Cameron-Erdős conjecture, Bull. London Math. Soc. 36 (2004), 769-778; A. A. Sapozhenko, The Cameron-Erdős conjecture, Dokl. Akad. Nauk 393 (2003), 749-752, abstract of arXiv:math/0304058 (Green): the number of sum-free subsets of {1, …, N} is O(2^{N/2}); erdosproblems.com/748: true, in fact f(n) ≪ 2^{n/2} (Green; Sapozhenko), with the trivial lower bound from subsets of the upper half, https://arxiv.org/abs/math/0304058.

Uses 1

Statement usesErdős Problem 748 on the number of sum-free sets

4 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.