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

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) : ThreeAPFree (frontier 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.

theorem threeAPFree_sphere {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [StrictConvexSpace ℝ E] (x : E) (r : ℝ) : ThreeAPFree (Metric.sphere x r)

Turning the sphere into 3AP-free 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 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

• 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 → ℕ) => ∑ 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

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 → ℕ) : (Behrend.map d) a = ∑ i : Fin n, a i * d ^ ↑i

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 + (∑ 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_injOn {n d : ℕ} : 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 ≤ ∑ i : Fin n, (d - 1) * (2 * d - 1) ^ ↑i

theorem Behrend.threeAPFree_sphere {n d k : ℕ} : ThreeAPFree ↑(Behrend.sphere n d k)

theorem Behrend.threeAPFree_image_sphere {n d k : ℕ} : ThreeAPFree ↑(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) : ∑ 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

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