The folded additive lemma

Monotonicity of the sum sets, the reflection -B = {m - b} and its effect on lowSums/highSums/collisions, and the inductive core_step that proves the folded additive lemma folded_additive.

Monotonicity of the sum sets

theorem Erdos865.foldedOK_subset {m : ℕ} {B C : Finset ℕ} (hB : FoldedOK m B) (h : C ⊆ B) : FoldedOK m C

theorem Erdos865.lowSums_mono {m : ℕ} {B C : Finset ℕ} (h : B ⊆ C) : lowSums m B ⊆ lowSums m C

theorem Erdos865.highSums_mono {m : ℕ} {B C : Finset ℕ} (h : B ⊆ C) : highSums m B ⊆ highSums m C

theorem Erdos865.collisions_mono {m : ℕ} {B C : Finset ℕ} (h : B ⊆ C) : collisions m B ⊆ collisions m C

theorem Erdos865.mem_lowSums_lt {m : ℕ} {B : Finset ℕ} {v : ℕ} (hv : v ∈ lowSums m B) : v < m

theorem Erdos865.mem_highSums_lt {m : ℕ} (_hm : 2 ≤ m) {B : Finset ℕ} (hB : FoldedOK m B) {v : ℕ} (hv : v ∈ highSums m B) : v < m

theorem Erdos865.sum_not_lowSums_erase {m : ℕ} {S : Finset ℕ} {α β : ℕ} (hαβ : α < β) (hmin2 : ∀ x ∈ S, x ≠ α → β ≤ x) : α + β ∉ lowSums m (S.erase α)

Reflection -B = {m - b}

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

The reflected set -B = {m - b : b ∈ B}.

Equations

• Erdos865.reflB m B = Finset.image (fun (b : ℕ) => m - b) B

theorem Erdos865.card_reflB {m : ℕ} {B : Finset ℕ} (hB : FoldedOK m B) : (reflB m B).card = B.card

theorem Erdos865.foldedOK_reflB {m : ℕ} (hm : 2 ≤ m) {B : Finset ℕ} (hB : FoldedOK m B) : FoldedOK m (reflB m B)

theorem Erdos865.lowSums_reflB {m : ℕ} (_hm : 2 ≤ m) {B : Finset ℕ} (hB : FoldedOK m B) : lowSums m (reflB m B) = Finset.image (fun (v : ℕ) => m - v) (highSums m B)

theorem Erdos865.highSums_reflB {m : ℕ} (hm : 2 ≤ m) {B : Finset ℕ} : highSums m (reflB m B) = Finset.image (fun (v : ℕ) => m - v) (lowSums m B)

theorem Erdos865.collisions_reflB_card {m : ℕ} (hm : 2 ≤ m) {B : Finset ℕ} (hB : FoldedOK m B) : (collisions m (reflB m B)).card = (collisions m B).card

The core inductive step

theorem Erdos865.core_step {m : ℕ} (hm : 2 ≤ m) {S : Finset ℕ} (hS : FoldedOK m S) {α β : ℕ} (hα : α ∈ S) (hβ : β ∈ S) (hαβ : α < β) (hmin : ∀ x ∈ S, α ≤ x) (hmin2 : ∀ x ∈ S, x ≠ α → β ≤ x) (hsum : α + β < m) (IH : ∀ (S' : Finset ℕ), FoldedOK m S' → S'.card < S.card → 4 * S'.card ≤ 4 * (collisions m S').card + m + 8) : 4 * S.card ≤ 4 * (collisions m S).card + m + 8

The folded additive lemma

theorem Erdos865.folded_additive {m : ℕ} (hm : 2 ≤ m) {B : Finset ℕ} (hB : FoldedOK m B) : 4 * B.card ≤ 4 * (collisions m B).card + m + 8