Distinct consecutive sums

DefinitionConsecutive sums#✓fully proved

Let \(k \in \mathbb{N}\) and let \(a_0, \dots, a_{k-1}\) be natural numbers. The consecutive sums of \(a\) form the finite set of natural numbers \(a_u + a_{u+1} + \dots + a_v\) for indices \(0 \le u \le v \le k - 1\).

def consecutiveSums {k : ℕ} (a : Fin k → ℕ) : Finset ℕ :=
  ((Finset.univ : Finset (Fin k × Fin k)).filter fun p => p.1 ≤ p.2).image
    fun p => ∑ i ∈ Finset.Icc p.1 p.2, a i

Used by 1

Used byErdős Problem 356

DefinitionErdős Problem 356#✓fully proved

The proposition that there is a real number \(c > 0\) such that for all sufficiently large \(n \in \mathbb{N}\) there exist \(k \in \mathbb{N}\) and natural numbers \(a_0 < a_1 < \dots < a_{k-1}\) with \(1 \le a_i \le n\) for every \(i\), whose set of consecutive sums \(a_u + a_{u+1} + \dots + a_v\) (for \(u \le v\)) has at least \(c n^2\) elements.

def manyDistinctConsecutiveSums : Prop :=
  ∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in Filter.atTop, ∃ k : ℕ, ∃ a : Fin k → ℕ, StrictMono a ∧
    (∀ i, 1 ≤ a i ∧ a i ≤ n) ∧ c * (n : ℝ) ^ 2 ≤ (consecutiveSums a).card

Uses 1 · Used by 1

Statement usesConsecutive sums

Used byErdős Problem 356 has a positive answer

TheoremErdős Problem 356 has a positive answer#●ready to prove

There is a real number \(c > 0\) such that for all sufficiently large \(n \in \mathbb{N}\) there exist \(k \in \mathbb{N}\) and natural numbers \(a_0 < a_1 < \dots < a_{k-1}\) with \(1 \le a_i \le n\) for every \(i\), whose set of consecutive sums \(a_u + a_{u+1} + \dots + a_v\) (for \(u \le v\)) has at least \(c n^2\) elements.

public theorem_wanted manyDistinctConsecutiveSums_holds : manyDistinctConsecutiveSums

Sources

• T. F. Bloom, Erdős Problems, Problem #356, https://www.erdosproblems.com/356 (status PROVED (LEAN)); resolution: A. Beker, On a problem of Erdős and Graham about consecutive sums in strictly increasing sequences, arXiv:2311.10087 (2023), erdosproblems.com/356: the original problem was solved in the affirmative by Beker, https://arxiv.org/abs/2311.10087.

Uses 1

Statement usesErdős Problem 356

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.