sIncreasingrTuples.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

33 declarations, 6 contain sorry, 0 declared as axioms

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

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

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, Combinatorics, Probability and Computing (2021), 686-721

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100SolvedSet1.lean

def Arxiv.«1609.08688».lt₂ Let $a = (a_1, a_2, a_3)$ and $b = (b_1, b_2, b_3)$ be two triples of integers line 43 source
Source documentation
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 coordinates $i$.

no axioms what this means
Statement uses: LT, Fin, OfNat.ofNat, Nat
Proof uses: Exists, And, Ne, LT.lt
2 instances, coercions and auxiliary constants left out.
```
def lt₂ {α : Type*} [LT α] (a b : Fin 3 → α) : Prop :=
…
```
theorem Arxiv.«1609.08688».not_lt₂ line 49 source
standard axioms: Quot.sound, propext what this means
Statement uses: LinearOrder, Fin, OfNat.ofNat, Nat, Iff, Not, Arxiv.«1609.08688».lt₂, Ne, LT.lt, LE.le
Proof uses: of_eq_true, Eq, Eq.trans, True, congrFun', congrArg, Exists, And, forall_congr, implies_congr, Eq.refl, iff_self
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Arxiv.«1609.08688».not_lt₂_of_forall_le line 53 source
standard axioms: Quot.sound, propext what this means
Statement uses: LinearOrder, Fin, OfNat.ofNat, Nat, LE.le, Not, Arxiv.«1609.08688».lt₂
Proof uses: Iff.mpr, Ne, LT.lt, Arxiv.«1609.08688».not_lt₂
16 instances, coercions and auxiliary constants left out.
theorem Arxiv.«1609.08688».not_lt₂_of_exists line 57 source
standard axioms: Quot.sound, propext what this means
Statement uses: LinearOrder, Fin, OfNat.ofNat, Nat, Ne, LE.le, Not, Arxiv.«1609.08688».lt₂
Proof uses: Iff.mpr, LT.lt, Arxiv.«1609.08688».not_lt₂, Eq, not_lt, Eq.rec, Or, Decidable.byContradiction
22 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem Arxiv.«1609.08688».not_lt₂_self line 67 source
standard axioms: Quot.sound, propext what this means
Statement uses: LinearOrder, Fin, OfNat.ofNat, Nat, Not, Arxiv.«1609.08688».lt₂
Proof uses: of_eq_true, Eq.trans, Ne, LT.lt, LE.le, True, Eq, forall_congr, implies_congr, Eq.refl, False, implies_true
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Arxiv.«1609.08688».lt₂_example_1 For example, $(3, 3, 9) <_2 (5, 6, 1)$ line 72 source
Source documentation
For example, $(3, 3, 9) <_2 (5, 6, 1)$.

standard axioms: Quot.sound, propext what this means
Statement uses: Arxiv.«1609.08688».lt₂, Nat, Matrix.vecCons, OfNat.ofNat, Matrix.vecEmpty
Proof uses: Exists.intro, Fin, Exists, And, Ne, LT.lt, And.intro, zero_ne_one, of_eq_true, Eq.trans, True, congr, congrArg, eq_true_of_decide, Eq.refl, Bool, Bool.true, and_self
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem lt₂_example_1 : ![3, 3, 9] <₂ ![5, 6, 1] := ⟨0, 1, zero_ne_one, by simp⟩
…
```
theorem Arxiv.«1609.08688».lt₂_example_2 $(5, 6, 1) <_2 (7, 7, 7)$ line 76 source
Source documentation
$(5, 6, 1) <_2 (7, 7, 7)$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Arxiv.«1609.08688».lt₂, Nat, Matrix.vecCons, OfNat.ofNat, Matrix.vecEmpty
Proof uses: Exists.intro, Fin, Exists, And, Ne, LT.lt, And.intro, of_eq_true, Not, Eq, Eq.trans, False, True, congrArg, eq_false_of_decide, Eq.refl, Bool, Bool.false, not_false_eq_true, congr and 3 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem lt₂_example_2 : ![5, 6, 1] <₂ ![7, 7, 7] := ⟨0, 2, by simp, by simp⟩
…
```
theorem Arxiv.«1609.08688».lt₂_example_3 $(7, 7, 7) <_2 (7, 8, 9)$ line 80 source
Source documentation
$(7, 7, 7) <_2 (7, 8, 9)$

standard axioms: propext what this means
Statement uses: Arxiv.«1609.08688».lt₂, Nat, Matrix.vecCons, OfNat.ofNat, Matrix.vecEmpty
Proof uses: Exists.intro, Fin, Exists, And, Ne, LT.lt, And.intro, of_eq_true, Not, Eq, Eq.trans, False, True, congrArg, eq_false_of_decide, Eq.refl, Bool, Bool.false, not_false_eq_true, congr and 3 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem lt₂_example_3 : ![7, 7, 7] <₂ ![7, 8, 9] := ⟨1, 2, by simp, by simp⟩
…
```
theorem Arxiv.«1609.08688».not_lt₂_example but $(1, 2, 3)$ is not $2$-less than $(1, 2, 4)$ line 84 source
Source documentation
but $(1, 2, 3)$ is not $2$-less than $(1, 2, 4)$.

standard axioms: Quot.sound, propext what this means
Statement uses: Not, Arxiv.«1609.08688».lt₂, Nat, Matrix.vecCons, OfNat.ofNat, Matrix.vecEmpty
Proof uses: Arxiv.«1609.08688».not_lt₂_of_exists, Fin, zero_ne_one, of_eq_true, LE.le
27 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem not_lt₂_example : ¬![1, 2, 3] <₂ ![1, 2, 4] := not_lt₂_of_exists 0 1 zero_ne_one (by simp) (by simp)
…
```
Mentions: Arxiv.«1609.08688».not_lt₂_of_exists
theorem Arxiv.«1609.08688».not_trans_lt₂_nat The $2$-less relation is not transitive on the naturals line 88 source
Source documentation
The $2$-less relation is not transitive on the naturals.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Fin, OfNat.ofNat, Nat, And, Arxiv.«1609.08688».lt₂, Not
Proof uses: Exists.intro, Matrix.vecCons, Matrix.vecEmpty, And.intro, Ne, LT.lt, zero_ne_one, of_eq_true, Eq.trans, True, congr, congrArg, LE.le, and_self, Eq, False, eq_false_of_decide, Eq.refl, Bool, Bool.false and 4 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem not_trans_lt₂_nat : ∃ (a b c : Fin 3 → ℕ),
    a <₂ b ∧ b <₂ c ∧ ¬a <₂ c :=
…
```
Mentions: c
def Arxiv.«1609.08688».IsIncreasing₂ Since the $2$-less relation is not transitive, we make a further definition to specify transivity line 97 source
Source documentation
Since the $2$-less relation is not transitive, we make a further definition to specify transivity.

no axioms what this means
Statement uses: LT, List, Fin, OfNat.ofNat, Nat
Proof uses: List.Pairwise, Arxiv.«1609.08688».lt₂
2 instances, coercions and auxiliary constants left out.
```
def IsIncreasing₂ {α : Type*} [LT α] (s : List (Fin 3 → α)) : Prop := s.Pairwise lt₂
…
```
Mentions: Arxiv.«1609.08688».lt₂
theorem Arxiv.«1609.08688».isIncreasing₂_nil line 100 source
standard axioms: propext what this means
Statement uses: LT, Arxiv.«1609.08688».IsIncreasing₂, List.nil, Fin, OfNat.ofNat, Nat
Proof uses: of_eq_true, List.Pairwise, Arxiv.«1609.08688».lt₂
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Arxiv.«1609.08688».isIncreasing₂_singleton line 104 source
standard axioms: Quot.sound, propext what this means
Statement uses: LT, Fin, OfNat.ofNat, Nat, Arxiv.«1609.08688».IsIncreasing₂, List.cons, List.nil
Proof uses: of_eq_true, List.Pairwise, Arxiv.«1609.08688».lt₂, Eq.trans, And, Membership.mem, List, True, congr, congrArg, forall_congr, False, implies_congr, Eq.refl, implies_true, and_self
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Arxiv.«1609.08688».isIncreasing₂_const_length line 108 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: LinearOrder, List, Fin, OfNat.ofNat, Nat, Arxiv.«1609.08688».IsIncreasing₂, Membership.mem, Eq, LT.lt, List.length
Proof uses: Decidable.byContradiction, Not, Exists, And, Ne, GetElem.getElem, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, HAdd.hAdd, HMul.hMul, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast and 61 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def Arxiv.«1609.08688».maximalLength Let $F(n)$ be the maximal length of a $2$-increasing sequence of triples with each coordinate belong to $[n]$ ($= \{1, 2, ..., n\}$) line 121 source
Source documentation
Let $F(n)$ be the maximal length of a $2$-increasing sequence of triples with each coordinate belong to $[n]$ ($= \{1, 2, ..., n\}$).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: SupSet.sSup, Set.ofPred, Exists, List, Fin, OfNat.ofNat, Membership.mem, LE.le, Set, Set.range, Set.Icc, Arxiv.«1609.08688».IsIncreasing₂, Eq, List.length
6 instances, coercions and auxiliary constants left out.
```
noncomputable def maximalLength (n : ℕ) : ℕ :=
…
```
theorem Arxiv.«1609.08688».maximalLength_zero line 127 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Arxiv.«1609.08688».maximalLength, OfNat.ofNat
Proof uses: List, Fin, Iff, And, Arxiv.«1609.08688».IsIncreasing₂, Not, Membership.mem, List.length, List.nil, Iff.intro, Eq.mpr, id, Eq.trans, congrArg, and_self, List.eq_nil_of_subset_nil, False, False.elim, of_eq_true, True and 33 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Arxiv.«1609.08688».maximalLength_one line 137 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Arxiv.«1609.08688».maximalLength, OfNat.ofNat
Proof uses: List, Fin, Iff, And, Arxiv.«1609.08688».IsIncreasing₂, Membership.mem, List.length, Or, List.cons, List.nil, Iff.intro, LT.lt, Eq.rec, Arxiv.«1609.08688».isIncreasing₂_const_length, dite, LE.le, Eq.mpr, id, Eq.trans, False and 53 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
theorem Arxiv.«1609.08688».maximalLength_four sorry line 155 source
depends on sorry what this means
Statement uses: Eq, Nat, Arxiv.«1609.08688».maximalLength, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Arxiv.«1609.08688».exists_pair_of_mem_Icc 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 line 161 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Fin, OfNat.ofNat, Nat, LE.le, Membership.mem, Set, Set.range, Set.Icc, GT.gt, List.length, HPow.hPow, Exists, And, Ne, Eq, GetElem.getElem, LT.lt
Proof uses: Prod, Prod.mk, Decidable.byContradiction, Not, Finset, SProd.sprod, Finset.Icc, Finset.card, Finset.univ, Eq.mpr, id, congr, congrArg, Eq.trans, HMul.hMul, Finset.card_product, HSub.hSub, HAdd.hAdd, Nat.card_Icc, Nat.add_sub_cancel and 12 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma 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 j : Fin s.length), i ≠ j ∧ s[i] 0 = s[j] 0 ∧ s[i] 1 = s[j] 1 := by
…
```
theorem Arxiv.«1609.08688».maximalLength_le For all $n$ we have $F(n) \leq n^2$ line 190 source
Source documentation
For all $n$ we have $F(n) \leq n^2$.
This is the upper bound in [GoLo21, Proposition 1.4], proved by applying the pigeonhole principle to the first two coordinates.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Arxiv.«1609.08688».maximalLength, HPow.hPow, OfNat.ofNat
Proof uses: dite, Eq.mpr, SupSet.sSup, Set.ofPred, Exists, List, Fin, Membership.mem, Set, Set.range, Set.Icc, Arxiv.«1609.08688».IsIncreasing₂, Eq, List.length, id, congrArg, Arxiv.«1609.08688».maximalLength.eq_1, csSup_le, Exists.intro, List.nil and 43 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
theorem maximalLength_le (n : ℕ) : F n ≤ n ^ 2 := by
…
```
theorem Arxiv.«1609.08688».maximalLength_ge_of_isSquare Moreover, whenever $n$ is a perfect square we have $F(n) \geq n^{3/2}$ sorry line 217 source
Source documentation
Moreover, whenever $n$ is a perfect square we have $F(n) \geq n^{3/2}$.

depends on sorry what this means
Statement uses: Nat, IsSquare, LE.le, HPow.hPow, Nat.sqrt, OfNat.ofNat, Arxiv.«1609.08688».maximalLength
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem maximalLength_ge_of_isSquare {n : ℕ} (h : IsSquare n) :
    n.sqrt ^ 3 ≤ F n := by
…
```
def Arxiv.«1609.08688».IsComparable₂ Two triples $t_1$ and $t_2$ are $2$-comparable if one of them is $2$-less than the other line 223 source
Source documentation
Two triples $t_1$ and $t_2$ are $2$-comparable if one of them is $2$-less than the other.

no axioms what this means
Statement uses: LT, Fin, OfNat.ofNat, Nat
Proof uses: Or, Arxiv.«1609.08688».lt₂
2 instances, coercions and auxiliary constants left out.
```
def IsComparable₂ {α : Type*} [LT α] (t₁ t₂ : Fin 3 → α) : Prop :=
…
```
def Arxiv.«1609.08688».IsComparableSet₂ A set of triples is $2$-comparable if any two distinct members of it are $2$-comparable line 227 source
Source documentation
A set of triples is $2$-comparable if any two distinct members of it are $2$-comparable.

no axioms what this means
Statement uses: LT, List, Fin, OfNat.ofNat, Nat
Proof uses: Membership.mem, Ne, Arxiv.«1609.08688».IsComparable₂
3 instances, coercions and auxiliary constants left out.
```
def IsComparableSet₂ {α : Type*} [LT α] (s : List (Fin 3 → α)) : Prop :=
…
```
theorem Arxiv.«1609.08688».maximalLength_le_isBigO $F(n) \leq n^2 / \exp(\Omega(\log^*(n)))$, i.e. there is a constant $c > 0$ such that $F(n) \leq n^2 / \exp(c \log^*(n))$ for all sufficiently large $n$ sorry line 234 source
Source documentation
$F(n) \leq n^2 / \exp(\Omega(\log^*(n)))$, i.e. there is a constant $c > 0$ such that $F(n) \leq n^2 / \exp(c \log^*(n))$ for all sufficiently large $n$.

depends on sorry what this means
Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, LE.le, Arxiv.«1609.08688».maximalLength, HDiv.hDiv, HPow.hPow, Real.exp, HMul.hMul, Real.iteratedLog, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem maximalLength_le_isBigO : ∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
    (F n : ℝ) ≤ (n : ℝ) ^ 2 / Real.exp (c * (Real.iteratedLog n : ℝ)) := by
…
```
Mentions: c, Real.iteratedLog
def Arxiv.«1609.08688».tripleProduct 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 ordered lexicographically line 240 source
Source documentation
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 ordered lexicographically.

standard axioms: Quot.sound what this means
Statement uses: Fin, OfNat.ofNat, Nat, Lex, Prod
Proof uses: Equiv, toLex, Prod.mk
5 instances, coercions and auxiliary constants left out.
```
def tripleProduct {α : Type*} (a b : Fin 3 → α) : Fin 3 → α ×ₗ α :=
…
```
theorem Arxiv.«1609.08688».tripleProduct_const line 244 source
standard axioms: Quot.sound what this means
Statement uses: Eq, Fin, OfNat.ofNat, Nat, Lex, Prod, Arxiv.«1609.08688».tripleProduct, Equiv, toLex, Prod.mk
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
theorem Arxiv.«1609.08688».tripleProduct_vecConst_const line 249 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Fin, OfNat.ofNat, Nat, Lex, Prod, Arxiv.«1609.08688».tripleProduct, Matrix.vecCons, Matrix.vecEmpty, Nat.succ, Equiv, toLex, Prod.mk
Proof uses: funext, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, Eq.refl, eq_of_heq, List.Mem.tail, False.elim, noConfusion_of_Nat and 2 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def Arxiv.«1609.08688».sequenceProduct We define the product line 258 source
Source documentation
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.

standard axioms: Quot.sound what this means
Statement uses: List, Fin, OfNat.ofNat, Nat, Lex, Prod
Proof uses: List.flatMap, List.map, Arxiv.«1609.08688».tripleProduct
2 instances, coercions and auxiliary constants left out.
```
def sequenceProduct {α : Type*} (s t : List (Fin 3 → α)) : List (Fin 3 → α ×ₗ α) :=
…
```
theorem Arxiv.«1609.08688».sequenceProduct_example line 264 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, List, Fin, OfNat.ofNat, Nat, Lex, Prod, Arxiv.«1609.08688».sequenceProduct, List.cons, Matrix.vecCons, Matrix.vecEmpty, List.nil, Nat.succ, Equiv, toLex, Prod.mk
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, List.flatMap, List.map, Arxiv.«1609.08688».tripleProduct, HAppend.hAppend, funext, List.map_cons, List.map_nil, List.flatMap_cons, congr, Arxiv.«1609.08688».tripleProduct_vecConst_const, List.flatMap_nil, List.append_nil, eq_self
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Arxiv.«1609.08688».isIncreasing₂_sequenceProduct_example The product of two $2$-increasing sequences is $2$-increasing; this is the point of ordering the pairs lexicographically line 271 source
Source documentation
The product of two $2$-increasing sequences is $2$-increasing; this is the point of ordering the pairs lexicographically.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Arxiv.«1609.08688».IsIncreasing₂, Lex, Prod, Nat, Arxiv.«1609.08688».sequenceProduct, List.cons, Fin, OfNat.ofNat, Matrix.vecCons, Matrix.vecEmpty, List.nil
Proof uses: id, List.Pairwise, Arxiv.«1609.08688».lt₂, List.flatMap, List.map, Arxiv.«1609.08688».tripleProduct, Equiv, toLex, Prod.mk, of_decide_eq_true, Exists, And, Ne, LT.lt, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem isIncreasing₂_sequenceProduct_example :
    IsIncreasing₂ ([![1, 1, 1], ![2, 2, 2]] ⊗₂ [![1, 1, 1], ![2, 2, 2]]) := by
…
```
Mentions: Arxiv.«1609.08688».IsIncreasing₂
theorem Arxiv.«1609.08688».maximalLength_pow Suppose that for some $n$ we have $F(n) = n ^ {\alpha}$ sorry line 279 source
Source documentation
Suppose that for some $n$ we have $F(n) = n ^ {\alpha}$. Then there are arbitrarily large $m$ such that $F(m) \geq m^{\alpha}$.

depends on sorry what this means
Statement uses: Nat, Real, LT.lt, OfNat.ofNat, Eq, Arxiv.«1609.08688».maximalLength, HPow.hPow, Filter.Frequently, LE.le, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem maximalLength_pow {n : ℕ} {e : ℝ} (hn : 1 < n) (h : F n = (n : ℝ) ^ e) :
    ∃ᶠ m : ℕ in Filter.atTop, (m : ℝ) ^ e ≤ F m := by
…
```
theorem Arxiv.«1609.08688».maximalLength_pow_eventually Moreover, for every $\beta < \alpha$ and all sufficiently large $m$ we have $F(m) \geq m^{\beta}$ sorry line 286 source
Source documentation
Moreover, for every $\beta < \alpha$ and all sufficiently large $m$ we have $F(m) \geq m^{\beta}$.

depends on sorry what this means
Statement uses: Nat, Real, LT.lt, OfNat.ofNat, Eq, Arxiv.«1609.08688».maximalLength, HPow.hPow, Filter.Eventually, LE.le, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem maximalLength_pow_eventually {n : ℕ} {e : ℝ} (hn : 1 < n) (h : F n = (n : ℝ) ^ e)
    {b : ℝ} (hb : b < e) :
    ∀ᶠ m : ℕ in Filter.atTop, (m : ℝ) ^ b ≤ F m := by
…
```
theorem Arxiv.«1609.08688».maximalLength_le_strong $F(n) \leq n^{3/2}$ sorry line 293 source
Source documentation
$F(n) \leq n^{3/2}$.

depends on sorry what this means
Statement uses: Nat, LE.le, Real, Arxiv.«1609.08688».maximalLength, HPow.hPow, Real.sqrt, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem maximalLength_le_strong (n : ℕ) : F n ≤ Real.sqrt n ^ 3 := by
…
```