Non-averaging sets

DefinitionNon-averaging sets#✓fully proved

A finite set \(A\) of natural numbers is non-averaging if no \(a \in A\) is the arithmetic mean of a nonempty set \(S \subseteq A \setminus \{a\}\), that is, \(\sum_{s \in S} s \ne |S| \cdot a\) for every \(a \in A\) and every nonempty \(S \subseteq A \setminus \{a\}\).

Equivalently, no element of \(A\) is the arithmetic mean of at least two distinct elements of \(A\).

def IsNonAveraging (A : Finset ℕ) : Prop :=
  ∀ a ∈ A, ∀ S ⊆ A.erase a, S.Nonempty → ∑ s ∈ S, s ≠ S.card * a

Used by 1

Used byErdős Problem 186 on non-averaging sets

DefinitionErdős Problem 186 on non-averaging sets#✓fully proved

For every \(\varepsilon > 0\) and every sufficiently large \(N\), the largest non-averaging subset of \(\{1, \dots, N\}\) has size between \(N^{1/4 - \varepsilon}\) and \(N^{1/4 + \varepsilon}\): some non-averaging subset of \(\{1, \dots, N\}\) has at least \(N^{1/4 - \varepsilon}\) elements, and every non-averaging subset of \(\{1, \dots, N\}\) has at most \(N^{1/4 + \varepsilon}\) elements. In short, the largest non-averaging subset of \(\{1, \dots, N\}\) has size \(N^{1/4 + o(1)}\).

def nonAveragingMaxSizeQuarterExponent : Prop :=
  ∀ ε : ℝ, 0 < ε → ∀ᶠ N : ℕ in atTop,
    (∃ A : Finset ℕ, A ⊆ Finset.Icc 1 N ∧ IsNonAveraging A ∧
      (N : ℝ) ^ ((1 : ℝ) / 4 - ε) ≤ A.card) ∧
    ∀ A : Finset ℕ, A ⊆ Finset.Icc 1 N → IsNonAveraging A →
      (A.card : ℝ) ≤ (N : ℝ) ^ ((1 : ℝ) / 4 + ε)

Uses 1 · Used by 1

Statement usesNon-averaging sets

Used byPham–Zakharov theorem on non-averaging sets

TheoremPham–Zakharov theorem on non-averaging sets#●ready to prove

For every \(\varepsilon > 0\) and every sufficiently large \(N\), some non-averaging subset of \(\{1, \dots, N\}\) has at least \(N^{1/4 - \varepsilon}\) elements, and every non-averaging subset of \(\{1, \dots, N\}\) has at most \(N^{1/4 + \varepsilon}\) elements. Thus the largest non-averaging subset of \(\{1, \dots, N\}\) has size \(N^{1/4 + o(1)}\).

Bosznay constructed non-averaging subsets of \(\{1, \dots, N\}\) of size \(\gg N^{1/4}\), and Pham and Zakharov proved the matching upper bound \(N^{1/4 + o(1)}\).

public theorem_wanted nonAveragingMaxSizeQuarterExponent_holds : nonAveragingMaxSizeQuarterExponent

Sources

• T. F. Bloom, Erdős Problems, Problem #186, https://www.erdosproblems.com/186 (status SOLVED); resolution: H. T. Pham and D. Zakharov, Sharp bound for the Erdős-Straus non-averaging set problem, Geom. Funct. Anal. 35 (2025), 1712-1738, arXiv:2410.14624 (upper bound); Á. P. Bosznay, On the lower estimation of non-averaging sets, Acta Math. Hungar. 53 (1989), 155-157 (lower bound), Pham-Zakharov main theorem: the largest non-averaging subset of {1, …, n} has size n^{1/4 + o(1)}; erdosproblems.com/186: N^{1/4} ≪ F(N) ≪ N^{1/4 + o(1)}, https://arxiv.org/abs/2410.14624.

Uses 1

Statement usesErdős Problem 186 on non-averaging sets

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.