Definitions for the sharp 5/8 bound (Erdős 865)

Basic objects for the pairwise-sums problem: pairwise-sum triples and triple-free sets (HasTriple, IsTripleFree), the folded sum sets lowSums/highSums/collisions, the hypothesis FoldedOK, and the folding sets Xset/Yset/Bset/Eset.

def Erdos865.HasTriple (A : Finset ℕ) : Prop

A contains a pairwise-sum triple: distinct a, b, c ∈ A with a+b, a+c, b+c ∈ A.

Equations

• Erdos865.HasTriple A = ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ a + b ∈ A ∧ a + c ∈ A ∧ b + c ∈ A

def Erdos865.IsTripleFree (A : Finset ℕ) : Prop

A is triple-free if it contains no pairwise-sum triple.

Equations

• Erdos865.IsTripleFree A = ¬Erdos865.HasTriple A

Folded additive lemma definitions

def Erdos865.lowSums (m : ℕ) (B : Finset ℕ) : Finset ℕ

Non-wrapped pair sums x + y (x ≠ y, both in B, x + y < m).

Equations

• Erdos865.lowSums m B = Finset.image (fun (p : ℕ × ℕ) => p.1 + p.2) ({p ∈ B ×ˢ B | p.1 ≠ p.2 ∧ p.1 + p.2 < m})

def Erdos865.highSums (m : ℕ) (B : Finset ℕ) : Finset ℕ

Wrapped pair sums x + y - m (x ≠ y, both in B, x + y > m).

Equations

• Erdos865.highSums m B = Finset.image (fun (p : ℕ × ℕ) => p.1 + p.2 - m) ({p ∈ B ×ˢ B | p.1 ≠ p.2 ∧ m < p.1 + p.2})

def Erdos865.collisions (m : ℕ) (B : Finset ℕ) : Finset ℕ

Residues arising both as a non-wrapped and as a wrapped pair sum.

Equations

• Erdos865.collisions m B = Erdos865.lowSums m B ∩ Erdos865.highSums m B

def Erdos865.FoldedOK (m : ℕ) (B : Finset ℕ) : Prop

The hypothesis (1.1) of the folded additive lemma: B ⊆ {1,…,m-1} and for all distinct x, y ∈ B, x + y ≠ m and the residue of x + y mod m is not in B.

Equations

• Erdos865.FoldedOK m B = ((∀ b ∈ B, 1 ≤ b ∧ b < m) ∧ ∀ x ∈ B, ∀ y ∈ B, x ≠ y → x + y ≠ m ∧ (x + y) % m ∉ B)

Folding definitions

def Erdos865.Xset (A : Finset ℕ) (h : ℕ) : Finset ℕ

X = {r : 1 ≤ r < h, r ∈ A}.

Equations

• Erdos865.Xset A h = {r ∈ Finset.Ico 1 h | r ∈ A}

def Erdos865.Yset (A : Finset ℕ) (N h : ℕ) : Finset ℕ

Y = {r : 1 ≤ r < h, h + r ≤ N, h + r ∈ A}.

Equations

• Erdos865.Yset A N h = {r ∈ Finset.Ico 1 h | h + r ≤ N ∧ h + r ∈ A}

def Erdos865.Bset (A : Finset ℕ) (N h : ℕ) : Finset ℕ

B_h = X ∩ Y.

Equations

• Erdos865.Bset A N h = Erdos865.Xset A h ∩ Erdos865.Yset A N h

def Erdos865.Eset (A : Finset ℕ) (N h : ℕ) : Finset ℕ

E = [1, h-1] \ (X ∪ Y).

Equations

• Erdos865.Eset A N h = Finset.Ico 1 h \ (Erdos865.Xset A h ∪ Erdos865.Yset A N h)