The length of an $s$-increasing sequence of $r$-tuples

This file contains the formalisation of [GoLo21] up to and including Conjecture 1.8

[GoLo21] W.T. Gowers and J. Long, The length of an $s$-increasing sequence of $r$-tuples, Combinatorics, Probability and Computing (2021), 686-721.

References:

• arxiv/1609.08688 The length of an $s$-increasing sequence of $r$-tuples by W. T. Gowers, J. Long
• GoLo21 The length of an $s$-increasing sequence of $r$-tuples by W. T. Gowers, J. Long, 2021

def Arxiv.id160908688.lt₂ {α : Type u_1} [LT α] (a b : Fin 3 → α) : Prop

Let $a = (a_1, a_2, a_3)$ and $b = (b_1, b_2, b_3)$ be two triples of integers. Say that $a$ is $2$-less than $b$, or $a <_2 b$, if $a_i < b_i$ for at least two co-ordinates $i$.

Equations

• Arxiv.id160908688.lt₂ a b = ∃ (i : Fin 3) (j : Fin 3), i ≠ j ∧ a i < b i ∧ a j < b j

@[simp]

theorem Arxiv.id160908688.not_lt₂ {α : Type u_1} [LinearOrder α] {a b : Fin 3 → α} : ¬lt₂ a b ↔ ∀ (i j : Fin 3), i ≠ j → a i < b i → b j ≤ a j

theorem Arxiv.id160908688.not_lt₂_of_forall_le {α : Type u_1} [LinearOrder α] {a b : Fin 3 → α} (h : ∀ (i : Fin 3), b i ≤ a i) : ¬lt₂ a b

theorem Arxiv.id160908688.not_lt₂_of_exists {α : Type u_1} [LinearOrder α] {a b : Fin 3 → α} (i j : Fin 3) (hij : i ≠ j) (hi : b i ≤ a i) (hj : b j ≤ a j) : ¬lt₂ a b

theorem Arxiv.id160908688.not_lt₂_self {α : Type u_1} [LinearOrder α] (a : Fin 3 → α) : ¬lt₂ a a

theorem Arxiv.id160908688.not_trans_lt₂_nat : ∃ (a : Fin 3 → ℕ) (b : Fin 3 → ℕ) (c : Fin 3 → ℕ), lt₂ a b ∧ lt₂ b c ∧ ¬lt₂ a c

The $2$-less relation is not transitive on the naturals.

def Arxiv.id160908688.IsIncreasing₂ {α : Type u_1} [LT α] (s : List (Fin 3 → α)) : Prop

Since the $2$-less relation is not transitive, we make a further definition to specify transivity.

Equations

• Arxiv.id160908688.IsIncreasing₂ s = List.Pairwise Arxiv.id160908688.lt₂ s

@[simp]

theorem Arxiv.id160908688.isIncreasing₂_nil {α : Type u_1} [LT α] : IsIncreasing₂ []

@[simp]

theorem Arxiv.id160908688.isIncreasing₂_singleton {α : Type u_1} [LT α] (a : Fin 3 → α) : IsIncreasing₂ [a]

theorem Arxiv.id160908688.isIncreasing₂_const_length {α : Type u_1} [LinearOrder α] {val : α} {s : List (Fin 3 → α)} (h : IsIncreasing₂ s) (h_const : ∀ a ∈ s, ∀ (j : Fin 3), a j = val) : s.length < 2

noncomputable def Arxiv.id160908688.maximalLength (n : ℕ) : ℕ

Let $F(n)$ be the maximal length of a $2$-increasing sequence of triples with each coordinate belong to $[n]$ ($= \{1, 2, ..., n\}$).

Equations

• Arxiv.id160908688.maximalLength n = sSup {x : ℕ | ∃ (s : List (Fin 3 → ℕ)) (_ : ∀ a ∈ s, Set.range a ⊆ Set.Icc 1 n) (_ : Arxiv.id160908688.IsIncreasing₂ s), s.length = x}

theorem Arxiv.id160908688.exists_pair_of_mem_Icc {s : List (Fin 3 → ℕ)} {n : ℕ} (hn : 2 ≤ n) (hs₁ : ∀ a ∈ s, Set.range a ⊆ Set.Icc 1 n) (hs₂ : s.length > n ^ 2) : ∃ (i : Fin s.length) (j : Fin s.length), i ≠ j ∧ s[i] 0 = s[j] 0 ∧ s[i] 1 = s[j] 1

In a set of more than $n^2$ triples with coordinates from $\{1, ..., n\}$ we must have two triples that are equal in their first two coordinates.

theorem Arxiv.id160908688.maximalLength_le (n : ℕ) : maximalLength n ≤ n ^ 2

For all $n$ we have $F(n) \leq n^2$.

theorem Arxiv.id160908688.maximalLength_ge_of_isSquare {n : ℕ} (h : IsSquare n) : n.sqrt ^ 3 ≤ maximalLength n

Moreover, whenever $n$ is a perfect square we have $F(n) \geq n^{3/2}$.

def Arxiv.id160908688.IsComparable₂ {α : Type u_1} [LT α] (t₁ t₂ : Fin 3 → α) : Prop

Two triples $t_1$ and $t_2$ are $2$-comparable if one of them is $2$-less than the other.

Equations

• Arxiv.id160908688.IsComparable₂ t₁ t₂ = (Arxiv.id160908688.lt₂ t₁ t₂ ∨ Arxiv.id160908688.lt₂ t₂ t₁)

def Arxiv.id160908688.IsComparableSet₂ {α : Type u_1} [LT α] (s : List (Fin 3 → α)) : Prop

A set of triples is $2$-comparable if any two of them are $2$-comparable.

Equations

• Arxiv.id160908688.IsComparableSet₂ s = ∃ (t₁ : Fin 3 → α) (t₂ : Fin 3 → α), t₁ ≠ t₂ ∧ t₁ ∈ s ∧ t₂ ∈ s ∧ Arxiv.id160908688.IsComparable₂ t₁ t₂

theorem Arxiv.id160908688.maximalLength_le_isBigO : ∃ (Ω : ℕ → ℝ), (fun (n : ℕ) => ↑(↑n).iteratedLog) =O[Filter.atTop] Ω ∧ ∀ (n : ℕ), ↑(maximalLength n) ≤ ↑n ^ 2 / Real.exp (Ω n)

$F(n) \leq n^2 / \exp(\Omega(\log^*(n)))$.

def Arxiv.id160908688.tripleProduct {α : Type u_1} (a b : Fin 3 → α) : Lex ((i : Fin 3) → (fun (x : Fin 3) => α × α) i)

We define the product of two triples $(a, b, c)$ and $(d, e, f)$ by $((a, d), (b, e), (c, f))$, where the pairs are arranged in lexicographical order.

Equations

• Arxiv.id160908688.tripleProduct a b = toLex (Pi.prod a b)

@[simp]

theorem Arxiv.id160908688.tripleProduct_const {α : Type u_1} (a : α) : (tripleProduct (fun (x : Fin 3) => a) fun (x : Fin 3) => a) = toLex fun (x : Fin 3) => (a, a)

@[simp]

theorem Arxiv.id160908688.tripleProduct_vecConst_const {α : Type u_1} (a : α) : tripleProduct ![a, a, a] ![a, a, a] = toLex ![(a, a), (a, a), (a, a)]

def Arxiv.id160908688.sequenceProduct {α : Type u_1} (s t : List (Fin 3 → α)) : Lex (List (Lex ((i : Fin 3) → (fun (x : Fin 3) => α × α) i)))

We define the product $\otimes$ of two sequences $(a_i, b_i, c_i)$ and $(d_i, e_i, f_i)$ by the sequence $((a_i, d_j), (b_i, e_j), (c_i, f_j))$, where the indices $(i, j)$ are arranged lexicographically, and the pairs are also ordered lexicographically.

Equations

• Arxiv.id160908688.sequenceProduct s t = toLex (List.flatMap (fun (a : Fin 3 → α) => List.map (Arxiv.id160908688.tripleProduct a) t) s)

theorem Arxiv.id160908688.maximalLength_pow {n : ℕ} {e : ℝ} (hn : 1 < n) (h : ↑(maximalLength n) = ↑n ^ e) : ∀ᶠ (m : ℕ) in Filter.atTop, ↑m ^ e ≤ ↑(maximalLength m)

Suppose that for some $n$ we have $F(n) = n ^ {\alpha}$. Then there are arbitrarily large $m$ such that $F(m) \geq m^{\alpha}$.

theorem Arxiv.id160908688.maximalLength_le_strong (n : ℕ) : ↑(maximalLength n) ≤ √↑n ^ 3

$F(n) \leq n^{3/2}$.