Balanced subset sums in finite abelian groups

DefinitionNumber of subsets with a given sum#✓fully proved

For a finite subset \(A\) of an abelian group \(G\) and an element \(g \in G\), \(F_A(g)\) is the number of subsets \(S \subseteq A\), the empty set included, whose elements sum to \(g\), that is, with \(\sum_{x \in S} x = g\).

noncomputable def subsetSumCount {G : Type*} [AddCommGroup G] (A : Finset G) (g : G) : ℕ :=
  (A.powerset.filter fun S => ∑ x ∈ S, x = g).card

Used by 1

Used by\(\varepsilon\)-balanced subsets of a finite abelian group

Definition\(\varepsilon\)-balanced subsets of a finite abelian group#✓fully proved

Let \(G\) be a finite abelian group with \(N = |G|\) elements and let \(\varepsilon\) be a real number. A subset \(A \subseteq G\) is \(\varepsilon\)-balanced when, for every \(g \in G\), the number \(F_A(g)\) of subsets of \(A\) whose elements sum to \(g\) satisfies \(\left| F_A(g) - 2^{|A|}/N \right| \le \varepsilon \cdot 2^{|A|}/N\).

def IsBalanced {G : Type*} [AddCommGroup G] [Fintype G] (ε : ℝ) (A : Finset G) : Prop :=
  ∀ g : G, |(subsetSumCount A g : ℝ) - 2 ^ A.card / Fintype.card G| ≤
    ε * (2 ^ A.card / Fintype.card G)

Uses 1 · Used by 2

Statement usesNumber of subsets with a given sum

Used byProbability that a random subset is balanced · Erdős Problem 1179 (balanced subset sums of random subsets)

DefinitionProbability that a random subset is balanced#✓fully proved

For a finite abelian group \(G\), a real number \(\varepsilon\) and a natural number \(k\), this is the number of \(\varepsilon\)-balanced \(k\)-element subsets of \(G\) divided by the number of all \(k\)-element subsets of \(G\), that is, the probability that a uniformly random \(k\)-element subset of \(G\) is \(\varepsilon\)-balanced. When \(k > |G|\) there are no \(k\)-element subsets and the value is \(0\).

noncomputable def balancedProbability (G : Type*) [AddCommGroup G] [Fintype G] (ε : ℝ) (k : ℕ) :
    ℝ :=
  (((univ : Finset G).powersetCard k).filter (IsBalanced ε)).card /
    ((univ : Finset G).powersetCard k).card

Uses 1 · Used by 1

Statement uses\(\varepsilon\)-balanced subsets of a finite abelian group

Used byErdős Problem 1179 (balanced subset sums of random subsets)

DefinitionErdős Problem 1179 (balanced subset sums of random subsets)#✓fully proved

The statement of Erdős Problem 1179 is the proposition that, for every real \(\varepsilon\) with \(0 < \varepsilon < 1\), the following two bounds hold. Upper bound: there is a function \(k : \mathbb{N} \to \mathbb{N}\) with \(k(N) / \log_2 N \to 1\) as \(N \to \infty\) such that, for every sequence \((G_i)_{i \in \mathbb{N}}\) of finite abelian groups with \(|G_i| \to \infty\), the probability that a uniformly random \(k(|G_i|)\)-element subset of \(G_i\) is \(\varepsilon\)-balanced tends to \(1\) as \(i \to \infty\). Lower bound: for every finite abelian group \(G\), every \(\varepsilon\)-balanced subset \(A \subseteq G\) satisfies \(|G| \le 2^{|A|}\).

def balancedSubsetSumsThresholdLogTwo : Prop :=
  ∀ ε : ℝ, 0 < ε → ε < 1 →
    (∃ k : ℕ → ℕ, Tendsto (fun N : ℕ => (k N : ℝ) / Real.logb 2 N) atTop (nhds 1) ∧
      ∀ (G : ℕ → Type) [∀ i, AddCommGroup (G i)] [∀ i, Fintype (G i)],
        Tendsto (fun i => Fintype.card (G i)) atTop atTop →
          Tendsto (fun i => balancedProbability (G i) ε (k (Fintype.card (G i)))) atTop (nhds 1)) ∧
    ∀ (G : Type) [AddCommGroup G] [Fintype G] (A : Finset G), IsBalanced ε A →
      Fintype.card G ≤ 2 ^ A.card

Uses 2 · Used by 1

Statement uses\(\varepsilon\)-balanced subsets of a finite abelian group · Probability that a random subset is balanced

Used byErdős Problem 1179 holds

TheoremErdős Problem 1179 holds#●ready to prove

For every real \(\varepsilon\) with \(0 < \varepsilon < 1\), the following two bounds hold. Upper bound: there is a function \(k : \mathbb{N} \to \mathbb{N}\) with \(k(N) / \log_2 N \to 1\) as \(N \to \infty\) such that, for every sequence \((G_i)_{i \in \mathbb{N}}\) of finite abelian groups with \(|G_i| \to \infty\), the probability that a uniformly random \(k(|G_i|)\)-element subset of \(G_i\) is \(\varepsilon\)-balanced tends to \(1\) as \(i \to \infty\). Lower bound: for every finite abelian group \(G\), every \(\varepsilon\)-balanced subset \(A \subseteq G\) satisfies \(|G| \le 2^{|A|}\).

Writing \(g_\varepsilon(N)\) for the least size for which a uniformly random subset of a group of order \(N\) is \(\varepsilon\)-balanced with probability tending to \(1\), Erdős and Hall proved \(g_\varepsilon(N) \le (1 + O_\varepsilon(\log \log \log N / \log \log N)) \log_2 N\), improving the bound \((2 + o(1)) \log_2 N + O_\varepsilon(1)\) of Erdős and Rényi; the lower bound holds because an \(\varepsilon\)-balanced set with \(\varepsilon < 1\) has every element of \(G\) as a subset sum. erdosproblems.com/1179 lists the problem as proved.

public theorem_wanted balancedSubsetSumsThresholdLogTwo_holds : balancedSubsetSumsThresholdLogTwo

Sources

• T. F. Bloom, Erdős Problems, Problem #1179, https://www.erdosproblems.com/1179 (status PROVED); resolution: P. Erdős and R. R. Hall, Probabilistic methods in group theory. II, Houston J. Math. 2 (1976), 173-180, erdosproblems.com/1179: g_ε(N) ≤ (1 + O_ε(log log log N / log log N)) log₂ N for all 0 < ε < 1.

Uses 1

Statement usesErdős Problem 1179 (balanced subset sums of random subsets)

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.