# Behrend's bound on Roth numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_roth_number_nat: 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 (add_salem_spencer_sphere). Then we can turn this set in fin n → ℕ into a set in ℕ using behrend.map, which preserves add_salem_spencer because it is an additive monoid homomorphism.

def behrend.box (n d : ) :

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

Equations
theorem behrend.mem_box {n d : } {x : fin n } :
x d (i : fin n), x i < d
@[simp]
theorem behrend.card_box {n d : } :
d).card = d ^ n
@[simp]
theorem behrend.box_zero {n : } :
behrend.box (n + 1) 0 =
def behrend.sphere (n d k : ) :

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

Equations
theorem behrend.sphere_zero_subset {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 : } :
k d
theorem behrend.norm_of_mem_sphere {n d k : } {x : fin n } (hx : x k) :
((pi_Lp.equiv 2 (λ (ᾰ : fin n), )).symm) (coe x) = k
theorem behrend.sphere_subset_preimage_metric_sphere {n d k : } :
d k) (λ (x : fin n ), ((pi_Lp.equiv 2 (λ (ᾰ : fin n), )).symm) (coe x)) ⁻¹' ( k)
@[simp]
theorem behrend.map_apply {n : } (d : ) (a : fin n ) :
(behrend.map d) a = finset.univ.sum (λ (i : fin n), a i * d ^ i)
def behrend.map {n : } (d : ) :

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

Equations
@[simp]
theorem behrend.map_zero (d : ) (a : fin 0 ) :
theorem behrend.map_succ {n d : } (a : fin (n + 1) ) :
(behrend.map d) a = a 0 + finset.univ.sum (λ (x : fin n), a x.succ * d ^ x) * d
theorem behrend.map_succ' {n d : } (a : fin (n + 1) ) :
theorem behrend.map_monotone {n : } (d : ) :
theorem behrend.map_mod {n d : } (a : fin n.succ ) :
(behrend.map d) a % d = a 0 % d
theorem behrend.map_eq_iff {n d : } {x₁ x₂ : fin n.succ } (hx₁ : (i : fin n.succ), x₁ i < d) (hx₂ : (i : fin n.succ), 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_inj_on {n d : } :
{x : fin n | (i : fin n), x i < d}
theorem behrend.map_le_of_mem_box {n d : } {x : fin n } (hx : x d) :
(behrend.map (2 * d - 1)) x finset.univ.sum (λ (i : fin n), (d - 1) * (2 * d - 1) ^ i)
theorem behrend.sum_sq_le_of_mem_box {n d : } {x : fin n } (hx : x d) :
finset.univ.sum (λ (i : fin n), x i ^ 2) n * (d - 1) ^ 2
theorem behrend.sum_eq {n d : } :
finset.univ.sum (λ (i : fin n), d * (2 * d + 1) ^ i) = ((2 * d + 1) ^ n - 1) / 2
theorem behrend.sum_lt {n d : } :
finset.univ.sum (λ (i : fin n), d * (2 * d + 1) ^ i) < (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.n_value and behrend.d_value.

theorem behrend.exists_large_sphere_aux (n d : ) :
(k : ) (H : k finset.range (n * (d - 1) ^ 2 + 1)), (d ^ n) / ((n * (d - 1) ^ 2) + 1) d k).card)
theorem behrend.exists_large_sphere (n d : ) :
(k : ), d ^ n / (n * d ^ 2) d k).card)
theorem behrend.bound_aux' (n d : ) :
d ^ n / (n * d ^ 2) (roth_number_nat ((2 * d - 1) ^ n))
theorem behrend.bound_aux {n d : } (hd : d 0) (hn : 2 n) :
d ^ (n - 2) / n (roth_number_nat ((2 * d - 1) ^ n))
theorem behrend.le_sqrt_log {N : } (hN : 4096 N) :
real.log (2 / (1 - 2 / rexp 1)) * (69 / 50) (real.log N)
theorem behrend.exp_neg_two_mul_le {x : } (hx : 0 < x) :
theorem behrend.div_lt_floor {x : } (hx : 2 / (1 - 2 / rexp 1) x) :
theorem behrend.ceil_lt_mul {x : } (hx : 50 / 19 x) :
x⌉₊ < 69 / 50 * x
noncomputable def behrend.n_value (N : ) :

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

Equations
noncomputable def behrend.d_value (N : ) :

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

Equations
theorem behrend.n_value_pos {N : } (hN : 2 N) :
theorem behrend.two_le_n_value {N : } (hN : 3 N) :
theorem behrend.three_le_n_value {N : } (hN : 64 N) :
theorem behrend.d_value_pos {N : } (hN₃ : 8 N) :
theorem behrend.le_N {N : } (hN : 2 N) :
(2 * - 1) ^ N
theorem behrend.bound {N : } (hN : 4096 N) :
theorem behrend.roth_lower_bound_explicit {N : } (hN : 4096 N) :
N * rexp ((-4) * (real.log N)) <
theorem behrend.exp_four_lt  :
rexp 4 < 64
theorem behrend.lower_bound_le_one' {N : } (hN : 2 N) (hN' : N 4096) :
N * rexp ((-4) * (real.log N)) 1
theorem behrend.lower_bound_le_one {N : } (hN : 1 N) (hN' : N 4096) :
N * rexp ((-4) * (real.log N)) 1
theorem behrend.roth_lower_bound {N : } :
N * rexp ((-4) * (real.log N))