Erdős sumset conjecture

DefinitionErdős Problem 109 (the Erdős sumset conjecture)#✓fully proved

The upper density of a set \(A \subseteq \mathbb{N}\) is \(\limsup_{N \to \infty} \lvert A \cap \{0, \dots, N - 1\} \rvert / N\). This is the statement that every set \(A \subseteq \mathbb{N}\) of positive upper density contains \(B + C = \{b + c \mid b \in B, c \in C\}\) for some infinite sets \(B, C \subseteq \mathbb{N}\).

def sumsetInPositiveUpperDensity : Prop :=
  ∀ A : Set ℕ, 0 < A.upperDensity → ∃ B C : Set ℕ, B.Infinite ∧ C.Infinite ∧ B + C ⊆ A

Uses 1 · Used by 1

Statement usesUpper density

Used byMoreira–Richter–Robertson theorem (the Erdős sumset conjecture)

TheoremMoreira–Richter–Robertson theorem (the Erdős sumset conjecture)#●ready to prove

The upper density of a set \(A \subseteq \mathbb{N}\) is \(\limsup_{N \to \infty} \lvert A \cap \{0, \dots, N - 1\} \rvert / N\). Every set \(A \subseteq \mathbb{N}\) of positive upper density contains \(B + C = \{b + c \mid b \in B, c \in C\}\) for some infinite sets \(B, C \subseteq \mathbb{N}\).

public theorem_wanted sumsetInPositiveUpperDensity_holds : sumsetInPositiveUpperDensity

Sources

• T. F. Bloom, Erdős Problems, Problem #109, https://www.erdosproblems.com/109 (status PROVED (LEAN)); resolution: J. Moreira, F. K. Richter and D. Robertson, A proof of a sumset conjecture of Erdős, Ann. of Math. (2) (2019), 605-652, main theorem (erdosproblems.com/109), https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos109.lean#L9074.

Uses 1

Statement usesErdős Problem 109 (the Erdős sumset conjecture)

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.