Documentation

Mathlib.Combinatorics.Additive.AP.Three.Behrend

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 #

References #

Tags #

3AP-free, Salem-Spencer, Behrend construction, arithmetic progression, sphere, strictly convex

theorem threeAPFree_frontier {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedField 𝕜] [TopologicalSpace E] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs₀ : IsClosed s) (hs₁ : StrictConvex 𝕜 s) :

The frontier of a closed strictly convex set only contains trivial arithmetic progressions. The idea is that an arithmetic progression is contained on a line and the frontier of a strictly convex set does not contain lines.

Turning the sphere into 3AP-free set #

We define Behrend.sphere, the intersection of the L2 sphere with the positive quadrant of integer points. Because the L2 closed ball is strictly convex, the L2 sphere and Behrend.sphere are 3AP-free (threeAPFree_sphere). Then we can turn this set in Fin n → ℕ into a set in using Behrend.map, which preserves ThreeAPFree 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
theorem Behrend.mem_box {n d : } {x : Fin n} :
x box n d ∀ (i : Fin n), x i < d
@[simp]
theorem Behrend.card_box {n d : } :
(box n d).card = d ^ n
@[simp]
theorem Behrend.box_zero {n : } :
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
@[simp]
theorem Behrend.sphere_zero_right (n k : ) :
sphere (n + 1) 0 k =
theorem Behrend.sphere_subset_box {n d k : } :
sphere n d k box n d
theorem Behrend.norm_of_mem_sphere {n d k : } {x : Fin n} (hx : x sphere n d k) :
theorem Behrend.sphere_subset_preimage_metric_sphere {n d k : } :
(sphere n d k) (fun (x : Fin n) => (WithLp.equiv 2 (Fin n)).symm (Nat.cast x)) ⁻¹' Metric.sphere 0 k
def Behrend.map {n : } (d : ) :
(Fin n) →+

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

Equations
  • Behrend.map d = { toFun := fun (a : Fin n) => i : Fin n, a i * d ^ i, map_zero' := , map_add' := }
@[simp]
theorem Behrend.map_apply {n : } (d : ) (a : Fin n) :
(map d) a = i : Fin n, a i * d ^ i
theorem Behrend.map_zero (d : ) (a : Fin 0) :
(map d) a = 0
theorem Behrend.map_succ {n d : } (a : Fin (n + 1)) :
(map d) a = a 0 + (∑ x : Fin n, a x.succ * d ^ x) * d
theorem Behrend.map_succ' {n d : } (a : Fin (n + 1)) :
(map d) a = a 0 + (map d) (a Fin.succ) * d
theorem Behrend.map_monotone {n : } (d : ) :
Monotone (map d)
theorem Behrend.map_mod {n d : } (a : Fin n.succ) :
(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) :
(map d) x₁ = (map d) x₂ x₁ 0 = x₂ 0 (map d) (x₁ Fin.succ) = (map d) (x₂ Fin.succ)
theorem Behrend.map_injOn {n d : } :
Set.InjOn (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 box n d) :
(map (2 * d - 1)) x i : Fin n, (d - 1) * (2 * d - 1) ^ i
theorem Behrend.threeAPFree_image_sphere {n d k : } :
ThreeAPFree (Finset.image (⇑(map (2 * d - 1))) (sphere n d k))
theorem Behrend.sum_sq_le_of_mem_box {n d : } {x : Fin n} (hx : x box n d) :
i : Fin n, x i ^ 2 n * (d - 1) ^ 2
theorem Behrend.sum_eq {n d : } :
i : Fin n, d * (2 * d + 1) ^ i = ((2 * d + 1) ^ n - 1) / 2
theorem Behrend.sum_lt {n d : } :
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 3AP-free 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 : ) :
kFinset.range (n * (d - 1) ^ 2 + 1), ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) (sphere n d k).card
theorem Behrend.exists_large_sphere (n d : ) :
∃ (k : ), ↑(d ^ n) / ↑(n * d ^ 2) (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.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
noncomputable def Behrend.dValue (N : ) :

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

Equations
theorem Behrend.nValue_pos {N : } (hN : 2 N) :
0 < nValue N
theorem Behrend.three_le_nValue {N : } (hN : 64 N) :
theorem Behrend.dValue_pos {N : } (hN₃ : 8 N) :
0 < dValue N
theorem Behrend.le_N {N : } (hN : 2 N) :
(2 * dValue N - 1) ^ nValue N N
theorem Behrend.bound {N : } (hN : 4096 N) :
N ^ (↑(nValue N))⁻¹ / Real.exp 1 < (dValue N)
theorem Behrend.roth_lower_bound_explicit {N : } (hN : 4096 N) :
N * Real.exp (-4 * (Real.log N)) < (rothNumberNat N)
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