# 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.

Instances For
theorem Behrend.mem_box {n : } {d : } {x : Fin n} :
x ∀ (i : Fin n), x i < d
@[simp]
theorem Behrend.card_box {n : } {d : } :
Finset.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 sqrt k with the integer points in the positive quadrant.

Instances For
@[simp]
theorem Behrend.sphere_zero_right (n : ) (k : ) :
Behrend.sphere (n + 1) 0 k =
theorem Behrend.sphere_subset_box {n : } {d : } {k : } :
theorem Behrend.norm_of_mem_sphere {n : } {d : } {k : } {x : Fin n} (hx : x ) :
(WithLp.equiv 2 (Fin n)).symm (Nat.cast x) =
theorem Behrend.sphere_subset_preimage_metric_sphere {n : } {d : } {k : } :
↑() (fun x => (WithLp.equiv 2 (Fin n)).symm (Nat.cast x)) ⁻¹' Metric.sphere 0 ()
@[simp]
theorem Behrend.map_apply {n : } (d : ) (a : Fin n) :
↑() a = Finset.sum Finset.univ fun i => a i * d ^ i
def Behrend.map {n : } (d : ) :
(Fin n) →+

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

Instances For
theorem Behrend.map_zero (d : ) (a : Fin 0) :
↑() a = 0
theorem Behrend.map_succ {n : } {d : } (a : Fin (n + 1)) :
↑() a = a 0 + (Finset.sum Finset.univ fun x => a () * d ^ x) * d
theorem Behrend.map_succ' {n : } {d : } (a : Fin (n + 1)) :
↑() a = a 0 + ↑() (a Fin.succ) * d
theorem Behrend.map_monotone {n : } (d : ) :
Monotone ↑()
theorem Behrend.map_mod {n : } {d : } (a : Fin ()) :
↑() a % d = a 0 % d
theorem Behrend.map_eq_iff {n : } {d : } {x₁ : Fin ()} {x₂ : Fin ()} (hx₁ : ∀ (i : Fin ()), x₁ i < d) (hx₂ : ∀ (i : Fin ()), x₂ i < d) :
↑() x₁ = ↑() x₂ x₁ 0 = x₂ 0 ↑() (x₁ Fin.succ) = ↑() (x₂ Fin.succ)
theorem Behrend.map_injOn {n : } {d : } {x : Fin n} :
Set.InjOn ↑() {x | ∀ (i : Fin n), x i < d}
theorem Behrend.map_le_of_mem_box {n : } {d : } {x : Fin n} (hx : x ) :
↑(Behrend.map (2 * d - 1)) x Finset.sum Finset.univ fun i => (d - 1) * (2 * d - 1) ^ i
theorem Behrend.addSalemSpencer_image_sphere {n : } {d : } {k : } {x : Fin n} :
AddSalemSpencer ↑(Finset.image (↑(Behrend.map (2 * d - 1))) ())
theorem Behrend.sum_sq_le_of_mem_box {n : } {d : } {x : Fin n} (hx : x ) :
(Finset.sum Finset.univ fun i => x i ^ 2) n * (d - 1) ^ 2
theorem Behrend.sum_eq {n : } {d : } :
(Finset.sum Finset.univ fun i => d * (2 * d + 1) ^ i) = ((2 * d + 1) ^ n - 1) / 2
theorem Behrend.sum_lt {n : } {d : } :
(Finset.sum Finset.univ fun i => d * (2 * d + 1) ^ i) < (2 * d + 1) ^ n
theorem Behrend.card_sphere_le_rothNumberNat (n : ) (d : ) (k : ) :
Finset.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, k Finset.range (n * (d - 1) ^ 2 + 1) ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ↑(Finset.card ())
theorem Behrend.exists_large_sphere (n : ) (d : ) :
k, d ^ n / ↑(n * d ^ 2) ↑(Finset.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.le_sqrt_log {N : } (hN : 4096 N) :
Real.log (2 / (1 - 2 / )) * (69 / 50) Real.sqrt (Real.log N)
theorem Behrend.exp_neg_two_mul_le {x : } (hx : 0 < x) :
theorem Behrend.div_lt_floor {x : } (hx : 2 / (1 - 2 / ) x) :
x / < 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.

Instances For
noncomputable def Behrend.dValue (N : ) :

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

Instances For
theorem Behrend.nValue_pos {N : } (hN : 2 N) :
theorem Behrend.two_le_nValue {N : } (hN : 3 N) :
theorem Behrend.three_le_nValue {N : } (hN : 64 N) :
theorem Behrend.dValue_pos {N : } (hN₃ : 8 N) :
theorem Behrend.le_N {N : } (hN : 2 N) :
( - 1) ^ N
theorem Behrend.bound {N : } (hN : 4096 N) :
N ^ (1 / ↑()) / < ↑()
theorem Behrend.roth_lower_bound_explicit {N : } (hN : 4096 N) :
N * Real.exp (-4 * Real.sqrt (Real.log N)) < ↑()
theorem Behrend.lower_bound_le_one' {N : } (hN : 2 N) (hN' : N 4096) :
N * Real.exp (-4 * Real.sqrt (Real.log N)) 1
theorem Behrend.lower_bound_le_one {N : } (hN : 1 N) (hN' : N 4096) :
N * Real.exp (-4 * Real.sqrt (Real.log N)) 1
theorem Behrend.roth_lower_bound {N : } :
N * Real.exp (-4 * Real.sqrt (Real.log N)) ↑()