mathlib3 documentation

combinatorics.additive.behrend

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 : ℕ) :

finset (fin n → ℕ)

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

Equations

behrend.box n d = fintype.pi_finset (λ (_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 sqrt k with the integer points in the positive quadrant.

Equations

behrend.sphere n d k = finset.filter (λ (x : fin n → ℕ), finset.univ.sum (λ (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) :

‖⇑((pi_Lp.equiv 2 (λ (ᾰ : fin n), ℝ)).symm) (coe ∘ x)‖ = √ ↑k

theorem behrend.sphere_subset_preimage_metric_sphere {n d k : ℕ} :

↑(behrend.sphere n d k) ⊆ (λ (x : fin n → ℕ), ⇑((pi_Lp.equiv 2 (λ (ᾰ : fin n), ℝ)).symm) (coe ∘ x)) ⁻¹' metric.sphere 0 (√ ↑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 : ℕ) :

(fin n → ℕ) →+ ℕ

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

Equations

behrend.map d = {to_fun := λ (a : fin n → ℕ), finset.univ.sum (λ (i : fin n), a i * d ^ ↑i), map_zero' := _, map_add' := _}

@[simp]

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.univ.sum (λ (x : fin n), a x.succ * 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 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 : ℕ} :

set.inj_on ⇑(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.univ.sum (λ (i : fin n), (d - 1) * (2 * d - 1) ^ ↑i)

theorem behrend.add_salem_spencer_sphere {n d k : ℕ} :

add_salem_spencer ↑(behrend.sphere n d k)

theorem behrend.add_salem_spencer_image_sphere {n d k : ℕ} :

add_salem_spencer ↑(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.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

theorem behrend.card_sphere_le_roth_number_nat (n d k : ℕ) :

(behrend.sphere n d k).card ≤ ⇑roth_number_nat ((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) ≤ ↑((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) ≤ ↑(⇑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.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 / rexp 1) ≤ 8

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) :

rexp ((-2) * x) < rexp (2 - ↑⌈x⌉₊) / ↑⌈x⌉₊

theorem behrend.div_lt_floor {x : ℝ} (hx : 2 / (1 - 2 / rexp 1) ≤ x) :

x / rexp 1 < ↑⌊x / 2⌋₊

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

behrend.n_value N = ⌈√ (real.log ↑N)⌉₊

noncomputable def behrend.d_value (N : ℕ) :

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

Equations

behrend.d_value N = ⌊↑N ^ (1 / ↑(behrend.n_value N)) / 2⌋₊

theorem behrend.n_value_pos {N : ℕ} (hN : 2 ≤ N) :

0 < behrend.n_value N

theorem behrend.two_le_n_value {N : ℕ} (hN : 3 ≤ N) :

2 ≤ behrend.n_value N

theorem behrend.three_le_n_value {N : ℕ} (hN : 64 ≤ N) :

3 ≤ behrend.n_value N

theorem behrend.d_value_pos {N : ℕ} (hN₃ : 8 ≤ N) :

0 < behrend.d_value N

theorem behrend.le_N {N : ℕ} (hN : 2 ≤ N) :

(2 * behrend.d_value N - 1) ^ behrend.n_value N ≤ N

theorem behrend.bound {N : ℕ} (hN : 4096 ≤ N) :

↑N ^ (1 / ↑(behrend.n_value N)) / rexp 1 < ↑(behrend.d_value N)

theorem behrend.roth_lower_bound_explicit {N : ℕ} (hN : 4096 ≤ N) :

↑N * rexp ((-4) * √ (real.log ↑N)) < ↑(⇑roth_number_nat N)

theorem behrend.exp_four_lt :

rexp 4 < 64

theorem behrend.four_zero_nine_six_lt_exp_sixteen :

4096 < rexp 16

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)) ≤ ↑(⇑roth_number_nat N)