Behrend's bound on Roth numbers

This file proves Behrend's lower bound on Roth numbers. This says that we can find a subset of {1, ..., n} of size n / exp (O (sqrt (log n))) which does not contain arithmetic progressions of length 3.

The idea is that the sphere (in the n dimensional Euclidean space) doesn't contain arithmetic progressions (literally) because the corresponding ball is strictly convex. Thus we can take integer points on that sphere and map them onto ℕ in a way that preserves arithmetic progressions (Behrend.map).

Main declarations

• Behrend.sphere: The intersection of the Euclidean sphere with the positive integer quadrant. This is the set that we will map on ℕ.
• Behrend.map: Given a natural number d, Behrend.map d : ℕⁿ → ℕ reads off the coordinates as digits in base d.
• Behrend.card_sphere_le_rothNumberNat: Implicit lower bound on Roth numbers in terms of Behrend.sphere.
• Behrend.roth_lower_bound: Behrend's explicit lower bound on Roth numbers.

References

• [Bryan Gillespie, Behrend’s Construction] (http://www.epsilonsmall.com/resources/behrends-construction/behrend.pdf)
• Behrend, F. A., "On sets of integers which contain no three terms in arithmetical progression"
• Wikipedia, Salem-Spencer set

Tags

Salem-Spencer, Behrend construction, arithmetic progression, sphere, strictly convex

Turning the sphere into a Salem-Spencer set

We define Behrend.sphere, the intersection of the $L^2$ sphere with the positive quadrant of integer points. Because the $L^2$ closed ball is strictly convex, the $L^2$ sphere and Behrend.sphere are Salem-Spencer (addSalemSpencer_sphere). Then we can turn this set in Fin n → ℕ into a set in ℕ using Behrend.map, which preserves AddSalemSpencer because it is an additive monoid homomorphism.

def Behrend.box (n : ℕ) (d : ℕ) : Finset (Fin n → ℕ)

The box {0, ..., d - 1}^n as a Finset.

Equations

• Behrend.box n d = Fintype.piFinset fun (x : Fin n) => Finset.range d

theorem Behrend.mem_box {n : ℕ} {d : ℕ} {x : Fin n → ℕ} : x ∈ Behrend.box n d ↔ ∀ (i : Fin n), x i < d

@[simp]

theorem Behrend.card_box {n : ℕ} {d : ℕ} : (Behrend.box n d).card = d ^ n

@[simp]

theorem Behrend.box_zero {n : ℕ} : Behrend.box (n + 1) 0 = ∅

def Behrend.sphere (n : ℕ) (d : ℕ) (k : ℕ) : Finset (Fin n → ℕ)

The intersection of the sphere of radius √k with the integer points in the positive quadrant.

Equations

• Behrend.sphere n d k = Finset.filter (fun (x : Fin n → ℕ) => (Finset.sum Finset.univ fun (i : Fin n) => x i ^ 2) = k) (Behrend.box n d)

theorem Behrend.sphere_zero_subset {n : ℕ} {d : ℕ} : Behrend.sphere n d 0 ⊆ 0

@[simp]

theorem Behrend.sphere_zero_right (n : ℕ) (k : ℕ) : Behrend.sphere (n + 1) 0 k = ∅

theorem Behrend.sphere_subset_box {n : ℕ} {d : ℕ} {k : ℕ} : Behrend.sphere n d k ⊆ Behrend.box n d

theorem Behrend.norm_of_mem_sphere {n : ℕ} {d : ℕ} {k : ℕ} {x : Fin n → ℕ} (hx : x ∈ Behrend.sphere n d k) : ‖(WithLp.equiv 2 (Fin n → ℝ)).symm (Nat.cast ∘ x)‖ = √↑k

theorem Behrend.sphere_subset_preimage_metric_sphere {n : ℕ} {d : ℕ} {k : ℕ} : ↑(Behrend.sphere n d k) ⊆ (fun (x : Fin n → ℕ) => (WithLp.equiv 2 (Fin n → ℝ)).symm (Nat.cast ∘ x)) ⁻¹' Metric.sphere 0 √↑k

@[simp]

theorem Behrend.map_apply {n : ℕ} (d : ℕ) (a : Fin n → ℕ) : (Behrend.map d) a = Finset.sum Finset.univ fun (i : Fin n) => a i * d ^ ↑i

def Behrend.map {n : ℕ} (d : ℕ) : (Fin n → ℕ) →+ ℕ

The map that appears in Behrend's bound on Roth numbers.

Equations

• Behrend.map d = { toZeroHom := { toFun := fun (a : Fin n → ℕ) => Finset.sum Finset.univ fun (i : Fin n) => a i * d ^ ↑i, map_zero' := ⋯ }, map_add' := ⋯ }

theorem Behrend.map_zero (d : ℕ) (a : Fin 0 → ℕ) : (Behrend.map d) a = 0

theorem Behrend.map_succ {n : ℕ} {d : ℕ} (a : Fin (n + 1) → ℕ) : (Behrend.map d) a = a 0 + (Finset.sum Finset.univ fun (x : Fin n) => a (Fin.succ x) * d ^ ↑x) * d

theorem Behrend.map_succ' {n : ℕ} {d : ℕ} (a : Fin (n + 1) → ℕ) : (Behrend.map d) a = a 0 + (Behrend.map d) (a ∘ Fin.succ) * d

theorem Behrend.map_monotone {n : ℕ} (d : ℕ) : Monotone ⇑(Behrend.map d)

theorem Behrend.map_mod {n : ℕ} {d : ℕ} (a : Fin (Nat.succ n) → ℕ) : (Behrend.map d) a % d = a 0 % d

theorem Behrend.map_eq_iff {n : ℕ} {d : ℕ} {x₁ : Fin (Nat.succ n) → ℕ} {x₂ : Fin (Nat.succ n) → ℕ} (hx₁ : ∀ (i : Fin (Nat.succ n)), x₁ i < d) (hx₂ : ∀ (i : Fin (Nat.succ n)), x₂ i < d) : (Behrend.map d) x₁ = (Behrend.map d) x₂ ↔ x₁ 0 = x₂ 0 ∧ (Behrend.map d) (x₁ ∘ Fin.succ) = (Behrend.map d) (x₂ ∘ Fin.succ)

theorem Behrend.map_injOn {n : ℕ} {d : ℕ} {x : Fin n → ℕ} : Set.InjOn ⇑(Behrend.map d) {x : Fin n → ℕ | ∀ (i : Fin n), x i < d}

theorem Behrend.map_le_of_mem_box {n : ℕ} {d : ℕ} {x : Fin n → ℕ} (hx : x ∈ Behrend.box n d) : (Behrend.map (2 * d - 1)) x ≤ Finset.sum Finset.univ fun (i : Fin n) => (d - 1) * (2 * d - 1) ^ ↑i

theorem Behrend.addSalemSpencer_sphere {n : ℕ} {d : ℕ} {k : ℕ} : AddSalemSpencer ↑(Behrend.sphere n d k)

theorem Behrend.addSalemSpencer_image_sphere {n : ℕ} {d : ℕ} {k : ℕ} {x : Fin n → ℕ} : AddSalemSpencer ↑(Finset.image (⇑(Behrend.map (2 * d - 1))) (Behrend.sphere n d k))

theorem Behrend.sum_sq_le_of_mem_box {n : ℕ} {d : ℕ} {x : Fin n → ℕ} (hx : x ∈ Behrend.box n d) : (Finset.sum Finset.univ fun (i : Fin n) => x i ^ 2) ≤ n * (d - 1) ^ 2

theorem Behrend.sum_eq {n : ℕ} {d : ℕ} : (Finset.sum Finset.univ fun (i : Fin n) => d * (2 * d + 1) ^ ↑i) = ((2 * d + 1) ^ n - 1) / 2

theorem Behrend.sum_lt {n : ℕ} {d : ℕ} : (Finset.sum Finset.univ fun (i : Fin n) => d * (2 * d + 1) ^ ↑i) < (2 * d + 1) ^ n

theorem Behrend.card_sphere_le_rothNumberNat (n : ℕ) (d : ℕ) (k : ℕ) : (Behrend.sphere n d k).card ≤ rothNumberNat ((2 * d - 1) ^ n)

Optimization

Now that we know how to turn the integer points of any sphere into a Salem-Spencer set, we find a sphere containing many integer points by the pigeonhole principle. This gives us an implicit bound that we then optimize by tweaking the parameters. The (almost) optimal parameters are Behrend.nValue and Behrend.dValue.

theorem Behrend.exists_large_sphere_aux (n : ℕ) (d : ℕ) : ∃ k ∈ Finset.range (n * (d - 1) ^ 2 + 1), ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(Behrend.sphere n d k).card

theorem Behrend.exists_large_sphere (n : ℕ) (d : ℕ) : ∃ (k : ℕ), ↑(d ^ n) / ↑(n * d ^ 2) ≤ ↑(Behrend.sphere n d k).card

theorem Behrend.bound_aux' (n : ℕ) (d : ℕ) : ↑(d ^ n) / ↑(n * d ^ 2) ≤ ↑(rothNumberNat ((2 * d - 1) ^ n))

theorem Behrend.bound_aux {n : ℕ} {d : ℕ} (hd : d ≠ 0) (hn : 2 ≤ n) : ↑d ^ (n - 2) / ↑n ≤ ↑(rothNumberNat ((2 * d - 1) ^ n))

theorem Behrend.log_two_mul_two_le_sqrt_log_eight : Real.log 2 * 2 ≤ √(Real.log 8)

theorem Behrend.two_div_one_sub_two_div_e_le_eight : 2 / (1 - 2 / Real.exp 1) ≤ 8

theorem Behrend.le_sqrt_log {N : ℕ} (hN : 4096 ≤ N) : Real.log (2 / (1 - 2 / Real.exp 1)) * (69 / 50) ≤ √(Real.log ↑N)

theorem Behrend.exp_neg_two_mul_le {x : ℝ} (hx : 0 < x) : Real.exp (-2 * x) < Real.exp (2 - ↑⌈x⌉₊) / ↑⌈x⌉₊

theorem Behrend.div_lt_floor {x : ℝ} (hx : 2 / (1 - 2 / Real.exp 1) ≤ x) : x / Real.exp 1 < ↑⌊x / 2⌋₊

theorem Behrend.ceil_lt_mul {x : ℝ} (hx : 50 / 19 ≤ x) : ↑⌈x⌉₊ < 1.38 * x

noncomputable def Behrend.nValue (N : ℕ) : ℕ

The (almost) optimal value of n in Behrend.bound_aux.

Equations

• Behrend.nValue N = ⌈√(Real.log ↑N)⌉₊

noncomputable def Behrend.dValue (N : ℕ) : ℕ

The (almost) optimal value of d in Behrend.bound_aux.

Equations

• Behrend.dValue N = ⌊↑N ^ (↑(Behrend.nValue N))⁻¹ / 2⌋₊

theorem Behrend.nValue_pos {N : ℕ} (hN : 2 ≤ N) : 0 < Behrend.nValue N

theorem Behrend.three_le_nValue {N : ℕ} (hN : 64 ≤ N) : 3 ≤ Behrend.nValue N

theorem Behrend.dValue_pos {N : ℕ} (hN₃ : 8 ≤ N) : 0 < Behrend.dValue N

theorem Behrend.le_N {N : ℕ} (hN : 2 ≤ N) : (2 * Behrend.dValue N - 1) ^ Behrend.nValue N ≤ N

theorem Behrend.bound {N : ℕ} (hN : 4096 ≤ N) : ↑N ^ (↑(Behrend.nValue N))⁻¹ / Real.exp 1 < ↑(Behrend.dValue N)

theorem Behrend.roth_lower_bound_explicit {N : ℕ} (hN : 4096 ≤ N) : ↑N * Real.exp (-4 * √(Real.log ↑N)) < ↑(rothNumberNat N)

theorem Behrend.exp_four_lt : Real.exp 4 < 64

theorem Behrend.four_zero_nine_six_lt_exp_sixteen : 4096 < Real.exp 16

theorem Behrend.lower_bound_le_one' {N : ℕ} (hN : 2 ≤ N) (hN' : N ≤ 4096) : ↑N * Real.exp (-4 * √(Real.log ↑N)) ≤ 1

theorem Behrend.lower_bound_le_one {N : ℕ} (hN : 1 ≤ N) (hN' : N ≤ 4096) : ↑N * Real.exp (-4 * √(Real.log ↑N)) ≤ 1

theorem Behrend.roth_lower_bound {N : ℕ} : ↑N * Real.exp (-4 * √(Real.log ↑N)) ≤ ↑(rothNumberNat N)