Balancing infinite families of sequences

DefinitionErdős Problem 178 (balancing infinite families of sequences)#✓fully proved

The statement that for every family \(a_0, a_1, a_2, \ldots\) of strictly increasing sequences of natural numbers there is a function \(f : \mathbb{N} \to \mathbb{Z}\) taking only the values \(1\) and \(-1\) such that for every \(d \in \mathbb{N}\) there is a natural number \(C\) with \(\left|\sum_{j < m} f(a_i(j))\right| \le C\) for all \(i < d\) and all \(m \in \mathbb{N}\).

Here \(a_i\) enumerates the infinite set \(A_i = \{a_i(0) < a_i(1) < \cdots\} \subseteq \mathbb{N}\) in increasing order, and the sum runs over the first \(m\) elements of \(A_i\).

def boundedDiscrepancyInfiniteFamily : Prop :=
  ∀ a : ℕ → ℕ → ℕ, (∀ i, StrictMono (a i)) →
    ∃ f : ℕ → ℤ, (∀ n, f n = 1 ∨ f n = -1) ∧
      ∀ d : ℕ, ∃ C : ℕ, ∀ i < d, ∀ m : ℕ, |∑ j ∈ Finset.range m, f (a i j)| ≤ C

Used by 1

Used byBeck's theorem on balancing infinite families of sequences (Erdős Problem 178)

TheoremBeck's theorem on balancing infinite families of sequences (Erdős Problem 178)#●ready to prove

For every family \(a_0, a_1, a_2, \ldots\) of strictly increasing sequences of natural numbers there is a function \(f : \mathbb{N} \to \mathbb{Z}\) taking only the values \(1\) and \(-1\) such that for every \(d \in \mathbb{N}\) there is a natural number \(C\) with \(\left|\sum_{j < m} f(a_i(j))\right| \le C\) for all \(i < d\) and all \(m \in \mathbb{N}\).

Beck proved this; he later showed that the bound \(C\) can be taken \(\ll d^{4 + \varepsilon}\).

public theorem_wanted boundedDiscrepancyInfiniteFamily_holds : boundedDiscrepancyInfiniteFamily

Sources

• T. F. Bloom, Erdős Problems, Problem #178, https://www.erdosproblems.com/178 (status PROVED (LEAN)); resolution: J. Beck, Balancing families of integer sequences, Combinatorica 1 (1981), 209-216, erdosproblems.com/178: solved by Beck [Be81]; Beck (2017) improved the bound to d^{4+ε}, https://doi.org/10.1007/BF02579326.

Uses 1

Statement usesErdős Problem 178 (balancing infinite families of sequences)

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.