The Ruzsa-Szemerédi problem

This file proves the lower bound of the Ruzsa-Szemerédi problem. The problem is to find the maximum number of edges that a graph on n vertices can have if all edges belong to at most one triangle.

The lower bound comes from turning the big 3AP-free set from Behrend's construction into a graph that has the property that every triangle gives a (possibly trivial) arithmetic progression on the original set.

Main declarations

• ruzsaSzemerediNumberNat n: Maximum number of edges a graph on n vertices can have such that each edge belongs to exactly one triangle.
• ruzsaSzemerediNumberNat_asymptotic_lower_bound: There exists a graph with n vertices and Ω((n ^ 2 * exp (-4 * sqrt (log n)))) edges such that each edge belongs to exactly one triangle.

The Ruzsa-Szemerédi number

noncomputable def ruzsaSzemerediNumber (α : Type u_1) [DecidableEq α] [Fintype α] : ℕ

The Ruzsa-Szemerédi number of a fintype is the maximum number of edges a locally linear graph on that type can have.

In other words, ruzsaSzemerediNumber α is the maximum number of edges a graph on α can have such that each edge belongs to exactly one triangle.

Equations

• ruzsaSzemerediNumber α = Nat.findGreatest (fun (m : ℕ) => ∃ (G : SimpleGraph α) (x : DecidableRel G.Adj), (G.cliqueFinset 3).card = m ∧ G.LocallyLinear) ((Fintype.card α).choose 3)

theorem ruzsaSzemerediNumber_le {α : Type u_1} [DecidableEq α] [Fintype α] : ruzsaSzemerediNumber α ≤ (Fintype.card α).choose 3

theorem ruzsaSzemerediNumber_spec {α : Type u_1} [DecidableEq α] [Fintype α] : ∃ (G : SimpleGraph α) (x : DecidableRel G.Adj), (G.cliqueFinset 3).card = ruzsaSzemerediNumber α ∧ G.LocallyLinear

theorem SimpleGraph.LocallyLinear.le_ruzsaSzemerediNumber {α : Type u_1} [DecidableEq α] [Fintype α] {G : SimpleGraph α} [DecidableRel G.Adj] (hG : G.LocallyLinear) : (G.cliqueFinset 3).card ≤ ruzsaSzemerediNumber α

theorem ruzsaSzemerediNumber_mono {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [Fintype α] [Fintype β] (f : α ↪ β) : ruzsaSzemerediNumber α ≤ ruzsaSzemerediNumber β

theorem ruzsaSzemerediNumber_congr {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [Fintype α] [Fintype β] (e : α ≃ β) : ruzsaSzemerediNumber α = ruzsaSzemerediNumber β

noncomputable def ruzsaSzemerediNumberNat (n : ℕ) : ℕ

The n-th Ruzsa-Szemerédi number is the maximum number of edges a locally linear graph on n vertices can have.

In other words, ruzsaSzemerediNumberNat n is the maximum number of edges a graph on n vertices can have such that each edge belongs to exactly one triangle.

Equations

• ruzsaSzemerediNumberNat n = ruzsaSzemerediNumber (Fin n)

@[simp]

theorem ruzsaSzemerediNumberNat_card {α : Type u_1} [DecidableEq α] [Fintype α] : ruzsaSzemerediNumberNat (Fintype.card α) = ruzsaSzemerediNumber α

theorem ruzsaSzemerediNumberNat_mono : Monotone ruzsaSzemerediNumberNat

theorem ruzsaSzemerediNumberNat_le {n : ℕ} : ruzsaSzemerediNumberNat n ≤ n.choose 3

@[simp]

theorem ruzsaSzemerediNumberNat_zero : ruzsaSzemerediNumberNat 0 = 0

@[simp]

theorem ruzsaSzemerediNumberNat_one : ruzsaSzemerediNumberNat 1 = 0

@[simp]

theorem ruzsaSzemerediNumberNat_two : ruzsaSzemerediNumberNat 2 = 0

The Ruzsa-Szemerédi construction

theorem addRothNumber_le_ruzsaSzemerediNumber (α : Type u_1) [Fintype α] [DecidableEq α] [CommRing α] [Fact (IsUnit 2)] : Fintype.card α * addRothNumber Finset.univ ≤ ruzsaSzemerediNumber (α ⊕ α ⊕ α)

theorem rothNumberNat_le_ruzsaSzemerediNumberNat (n : ℕ) : (2 * n + 1) * rothNumberNat n ≤ ruzsaSzemerediNumberNat (6 * n + 3)

theorem rothNumberNat_le_ruzsaSzemerediNumberNat' (n : ℕ) : (↑n / 3 - 2) * ↑(rothNumberNat ((n - 3) / 6)) ≤ ↑(ruzsaSzemerediNumberNat n)

Lower bound on the Ruzsa-Szemerédi problem in terms of 3AP-free sets.

If there exists a 3AP-free subset of [1, ..., (n - 3) / 6] of size m, then there exists a graph with n vertices and (n / 3 - 2) * m edges such that each edge belongs to exactly one triangle.

theorem ruzsaSzemerediNumberNat_lower_bound (n : ℕ) : (↑n / 3 - 2) * ↑((n - 3) / 6) * Real.exp (-4 * √(Real.log ↑((n - 3) / 6))) ≤ ↑(ruzsaSzemerediNumberNat n)

Explicit lower bound on the Ruzsa-Szemerédi problem.

There exists a graph with n vertices and (n / 3 - 2) * (n - 3) / 6 * exp (-4 * sqrt (log ((n - 3) / 6))) edges such that each edge belongs to exactly one triangle.

theorem ruzsaSzemerediNumberNat_asymptotic_lower_bound : (fun (n : ℕ) => ↑n ^ 2 * Real.exp (-4 * √(Real.log ↑n))) =O[Filter.atTop] fun (n : ℕ) => ↑(ruzsaSzemerediNumberNat n)

Asymptotic lower bound on the Ruzsa-Szemerédi problem.

There exists a graph with n vertices and Ω((n ^ 2 * exp (-4 * sqrt (log n)))) edges such that each edge belongs to exactly one triangle.