Erdős–Szekeres theorem

TheoremA positive natural number exceeds its predecessor#✓fully proved

For every natural number \(k > 0\), \(k - 1 < k\).

theorem sub_one_lt_of_pos {k : ℕ} (hk : 0 < k) : k - 1 < k
Used by 20
Used byExtending a decreasing subsequence · Length of the longest decreasing subsequence ending at a point · The longest decreasing subsequence ending at a point has length at least one · The longest decreasing subsequence ending at a point is attained · Longest decreasing subsequence lengths grow along a descent · Erdős–Szekeres theorem · Appending a later index keeps indices increasing · The last entry of an appended map · Entries of a strictly increasing index map lie at or below its last entry · Extending an increasing subsequence · Length of the longest increasing subsequence ending at a position · Longest increasing subsequences ending at a position have length at least one · The longest increasing subsequence ending at a position is attained · Longest increasing subsequence lengths increase strictly along increasing pairs · Decreasing subsequence ending at a position · Increasing subsequence ending at a position · The last value is the smallest along a strictly decreasing selection · Bound by the longest decreasing subsequence ending at a position · Bound by the longest increasing subsequence ending at a position · The last value is the largest along a strictly increasing selection

DefinitionIncreasing subsequence#✓fully proved

For \(f : \{0, \dots, N-1\} \to \mathbb{R}\) and \(k \in \mathbb{N}\), a map \(\varphi : \{0, \dots, k-1\} \to \{0, \dots, N-1\}\) is an increasing subsequence of \(f\) of length \(k\) when \(\varphi(i) < \varphi(j)\) and \(f(\varphi(i)) < f(\varphi(j))\) for all \(i < j\).

def IsIncrSubseq {N : ℕ} (f : Fin N → ℝ) (k : ℕ) (φ : Fin k → Fin N) : Prop :=
  (∀ i j : Fin k, i < j → φ i < φ j) ∧
  (∀ i j : Fin k, i < j → f (φ i) < f (φ j))
Used by 10
Used byErdős–Szekeres theorem · Extending an increasing subsequence · Length of the longest increasing subsequence ending at a position · Longest increasing subsequences ending at a position have length at least one · The longest increasing subsequence ending at a position is attained · Longest increasing subsequence lengths increase strictly along increasing pairs · Increasing subsequence ending at a position · Bound by the longest increasing subsequence ending at a position · One-term subsequences are increasing · Increasing subsequences of every smaller length

DefinitionDecreasing subsequence#✓fully proved

For \(f : \{0, \dots, N-1\} \to \mathbb{R}\) and \(k \in \mathbb{N}\), a map \(\varphi : \{0, \dots, k-1\} \to \{0, \dots, N-1\}\) is a decreasing subsequence of \(f\) of length \(k\) when \(\varphi(i) < \varphi(j)\) and \(f(\varphi(j)) < f(\varphi(i))\) for all \(i < j\).

def IsDecrSubseq {N : ℕ} (f : Fin N → ℝ) (k : ℕ) (φ : Fin k → Fin N) : Prop :=
  (∀ i j : Fin k, i < j → φ i < φ j) ∧
  (∀ i j : Fin k, i < j → f (φ j) < f (φ i))
Used by 10
Used byExtending a decreasing subsequence · Length of the longest decreasing subsequence ending at a point · The longest decreasing subsequence ending at a point has length at least one · The longest decreasing subsequence ending at a point is attained · Longest decreasing subsequence lengths grow along a descent · Erdős–Szekeres theorem · Decreasing subsequence ending at a position · Bound by the longest decreasing subsequence ending at a position · One-term subsequences are decreasing · Decreasing subsequences of every smaller length

DefinitionIncreasing subsequence ending at a position#✓fully proved

For \(f : \{0, \dots, N-1\} \to \mathbb{R}\), a position \(p\) and \(k \in \mathbb{N}\), this is the statement that \(k \ge 1\) and \(f\) has an increasing subsequence \(\varphi\) of length \(k\) (indices and values strictly increasing) ending at \(p\), that is, with \(\varphi(k-1) = p\).

def IsIncrEnd {N : ℕ} (f : Fin N → ℝ) (p : Fin N) (k : ℕ) : Prop :=
  ∃ (hk : 0 < k) (φ : Fin k → Fin N),
    IsIncrSubseq f k φ ∧ φ ⟨k - 1, sub_one_lt_of_pos hk⟩ = p
Uses 2 · Used by 6
Statement usesIncreasing subsequence · A positive natural number exceeds its predecessor
Used byErdős–Szekeres theorem · Extending an increasing subsequence · Length of the longest increasing subsequence ending at a position · The longest increasing subsequence ending at a position is attained · Longest increasing subsequence lengths increase strictly along increasing pairs · Bound by the longest increasing subsequence ending at a position

DefinitionDecreasing subsequence ending at a position#✓fully proved

For \(f : \{0, \dots, N-1\} \to \mathbb{R}\), a position \(p\) and \(k \in \mathbb{N}\), this is the statement that \(k \ge 1\) and \(f\) has a decreasing subsequence \(\varphi\) of length \(k\) (indices strictly increasing and values strictly decreasing) ending at \(p\), that is, with \(\varphi(k-1) = p\).

def IsDecrEnd {N : ℕ} (f : Fin N → ℝ) (p : Fin N) (k : ℕ) : Prop :=
  ∃ (hk : 0 < k) (φ : Fin k → Fin N),
    IsDecrSubseq f k φ ∧ φ ⟨k - 1, sub_one_lt_of_pos hk⟩ = p
Uses 2 · Used by 6
Statement usesDecreasing subsequence · A positive natural number exceeds its predecessor
Used byExtending a decreasing subsequence · Length of the longest decreasing subsequence ending at a point · The longest decreasing subsequence ending at a point is attained · Longest decreasing subsequence lengths grow along a descent · Erdős–Szekeres theorem · Bound by the longest decreasing subsequence ending at a position

TheoremNo strict pair in a one-element set#✓fully proved

There are no \(i, j \in \{0\}\) with \(i < j\).

theorem fin1_false {i j : Fin 1} (hij : i < j) : False
Used by 3
Used byErdős–Szekeres theorem · One-term subsequences are decreasing · One-term subsequences are increasing

TheoremOne-term subsequences are increasing#✓fully proved

For every real sequence \(f\) indexed by \(\{0, \dots, N-1\}\) and every position \(p\), the subsequence of length \(1\) consisting of the term at position \(p\) is a strictly increasing subsequence of \(f\).

theorem singleton_incr {N : ℕ} (f : Fin N → ℝ) (p : Fin N) :
    IsIncrSubseq f 1 (fun _ => p)
Uses 2 · Used by 3
Statement usesIncreasing subsequence
Proof usesNo strict pair in a one-element set
Used byLength of the longest increasing subsequence ending at a position · Longest increasing subsequences ending at a position have length at least one · The longest increasing subsequence ending at a position is attained

TheoremOne-term subsequences are decreasing#✓fully proved

For every real sequence \(f\) indexed by \(\{0, \dots, N-1\}\) and every position \(p\), the subsequence of length \(1\) consisting of the term at position \(p\) is a strictly decreasing subsequence of \(f\).

theorem singleton_decr {N : ℕ} (f : Fin N → ℝ) (p : Fin N) :
    IsDecrSubseq f 1 (fun _ => p)
Uses 2 · Used by 3
Statement usesDecreasing subsequence
Proof usesNo strict pair in a one-element set
Used byLength of the longest decreasing subsequence ending at a point · The longest decreasing subsequence ending at a point has length at least one · The longest decreasing subsequence ending at a point is attained

DefinitionLength of the longest increasing subsequence ending at a position#✓fully proved

For \(f : \{0, \dots, N-1\} \to \mathbb{R}\) and a position \(p\), this is the largest \(k \le N\) such that \(f\) has an increasing subsequence of length \(k\) ending at \(p\), where indices and values both increase strictly.

noncomputable def incrLen {N : ℕ} (f : Fin N → ℝ) (p : Fin N) : ℕ :=
  ((Finset.range (N + 1)).filter (IsIncrEnd f p)).max'
    ⟨1, by
      have hN : 0 < N := by
        have h := p.isLt
        omega
      rw [Finset.mem_filter, Finset.mem_range]
      exact ⟨by omega, by omega, fun _ => p, singleton_incr f p, rfl⟩⟩
Uses 4 · Used by 5
Statement usesIncreasing subsequence ending at a position · Increasing subsequence · One-term subsequences are increasing · A positive natural number exceeds its predecessor
Used byErdős–Szekeres theorem · Longest increasing subsequences ending at a position have length at least one · The longest increasing subsequence ending at a position is attained · Longest increasing subsequence lengths increase strictly along increasing pairs · Bound by the longest increasing subsequence ending at a position

DefinitionLength of the longest decreasing subsequence ending at a point#✓fully proved

For a real sequence \(f\) indexed by \(\{0, \dots, N-1\}\) and an index \(p\), this is the largest \(k\) such that \(f\) has a strictly decreasing subsequence of length \(k\) ending at \(p\), that is, indices \(i_1 < \dots < i_k = p\) with \(f(i_1) > \dots > f(i_k)\). The maximum exists: \(k = 1\) qualifies, and every such \(k\) is at most \(N\).

noncomputable def decrLen {N : ℕ} (f : Fin N → ℝ) (p : Fin N) : ℕ :=
  ((Finset.range (N + 1)).filter (IsDecrEnd f p)).max'
    ⟨1, by
      have hN : 0 < N := by
        have h := p.isLt
        omega
      rw [Finset.mem_filter, Finset.mem_range]
      exact ⟨by omega, by omega, fun _ => p, singleton_decr f p, rfl⟩⟩
Uses 4 · Used by 5
Statement usesDecreasing subsequence ending at a position · Decreasing subsequence · One-term subsequences are decreasing · A positive natural number exceeds its predecessor
Used byThe longest decreasing subsequence ending at a point has length at least one · The longest decreasing subsequence ending at a point is attained · Longest decreasing subsequence lengths grow along a descent · Erdős–Szekeres theorem · Bound by the longest decreasing subsequence ending at a position

TheoremSubsequences are no longer than the sequence#✓fully proved

If \(\varphi \colon \{0, \dots, k-1\} \to \{0, \dots, N-1\}\) is strictly increasing, that is \(\varphi(i) < \varphi(j)\) whenever \(i < j\), then \(k \le N\).

theorem subseqLen_le {N k : ℕ} {φ : Fin k → Fin N}
    (hidx : ∀ i j : Fin k, i < j → φ i < φ j) : k ≤ N
Used by 2
Used byBound by the longest decreasing subsequence ending at a position · Bound by the longest increasing subsequence ending at a position

TheoremThe longest increasing subsequence ending at a position is attained#✓fully proved

For every \(f : \{0, \dots, N-1\} \to \mathbb{R}\) and every position \(p\), \(f\) has an increasing subsequence ending at \(p\) whose length equals the length of the longest increasing subsequence of \(f\) ending at \(p\).

theorem incrLen_isEnd {N : ℕ} (f : Fin N → ℝ) (p : Fin N) :
    IsIncrEnd f p (incrLen f p)
Uses 5 · Used by 2
Statement usesIncreasing subsequence ending at a position · Length of the longest increasing subsequence ending at a position
Proof usesIncreasing subsequence · One-term subsequences are increasing · A positive natural number exceeds its predecessor
Used byErdős–Szekeres theorem · Longest increasing subsequence lengths increase strictly along increasing pairs

TheoremThe longest decreasing subsequence ending at a point is attained#✓fully proved

For every real sequence \(f\) indexed by \(\{0, \dots, N-1\}\) and every index \(p\), \(f\) has a strictly decreasing subsequence ending at \(p\) whose length equals the length of the longest strictly decreasing subsequence of \(f\) ending at \(p\).

theorem decrLen_isEnd {N : ℕ} (f : Fin N → ℝ) (p : Fin N) :
    IsDecrEnd f p (decrLen f p)
Uses 5 · Used by 2
Statement usesDecreasing subsequence ending at a position · Length of the longest decreasing subsequence ending at a point
Proof usesDecreasing subsequence · One-term subsequences are decreasing · A positive natural number exceeds its predecessor
Used byLongest decreasing subsequence lengths grow along a descent · Erdős–Szekeres theorem

TheoremBound by the longest increasing subsequence ending at a position#✓fully proved

Let \(f\) be a real sequence indexed by \(\{0, \dots, N-1\}\) and let \(p\) be a position. If \(f\) has a strictly increasing subsequence of length \(k\) ending exactly at \(p\), then \(k\) is at most the length of the longest strictly increasing subsequence of \(f\) ending at \(p\).

theorem le_incrLen {N : ℕ} (f : Fin N → ℝ) (p : Fin N) (k : ℕ)
    (h : IsIncrEnd f p k) : k ≤ incrLen f p
Uses 5 · Used by 2
Statement usesIncreasing subsequence ending at a position · Length of the longest increasing subsequence ending at a position
Proof usesIncreasing subsequence · A positive natural number exceeds its predecessor · Subsequences are no longer than the sequence
Used byLongest increasing subsequences ending at a position have length at least one · Longest increasing subsequence lengths increase strictly along increasing pairs

TheoremBound by the longest decreasing subsequence ending at a position#✓fully proved

Let \(f\) be a real sequence indexed by \(\{0, \dots, N-1\}\) and let \(p\) be a position. If \(f\) has a strictly decreasing subsequence of length \(k\) ending exactly at \(p\), then \(k\) is at most the length of the longest strictly decreasing subsequence of \(f\) ending at \(p\).

theorem le_decrLen {N : ℕ} (f : Fin N → ℝ) (p : Fin N) (k : ℕ)
    (h : IsDecrEnd f p k) : k ≤ decrLen f p
Uses 5 · Used by 2
Statement usesDecreasing subsequence ending at a position · Length of the longest decreasing subsequence ending at a point
Proof usesDecreasing subsequence · A positive natural number exceeds its predecessor · Subsequences are no longer than the sequence
Used byThe longest decreasing subsequence ending at a point has length at least one · Longest decreasing subsequence lengths grow along a descent

TheoremLongest increasing subsequences ending at a position have length at least one#✓fully proved

For every \(f : \{0, \dots, N-1\} \to \mathbb{R}\) and every position \(p\), the length of the longest increasing subsequence of \(f\) ending at \(p\) is at least \(1\).

theorem incrLen_ge_one {N : ℕ} (f : Fin N → ℝ) (p : Fin N) :
    1 ≤ incrLen f p
Uses 5 · Used by 1
Statement usesLength of the longest increasing subsequence ending at a position
Proof usesIncreasing subsequence · Bound by the longest increasing subsequence ending at a position · One-term subsequences are increasing · A positive natural number exceeds its predecessor
Used byErdős–Szekeres theorem

TheoremThe longest decreasing subsequence ending at a point has length at least one#✓fully proved

For every real sequence \(f\) indexed by \(\{0, \dots, N-1\}\) and every index \(p\), the length of the longest strictly decreasing subsequence of \(f\) ending at \(p\) is at least \(1\).

theorem decrLen_ge_one {N : ℕ} (f : Fin N → ℝ) (p : Fin N) :
    1 ≤ decrLen f p
Uses 5 · Used by 1
Statement usesLength of the longest decreasing subsequence ending at a point
Proof usesDecreasing subsequence · Bound by the longest decreasing subsequence ending at a position · One-term subsequences are decreasing · A positive natural number exceeds its predecessor
Used byErdős–Szekeres theorem

DefinitionAppending an entry to a map of indices#✓fully proved

Given \(\varphi : \{0, \dots, k-1\} \to \{0, \dots, N-1\}\) and \(p \in \{0, \dots, N-1\}\), the appended map on \(\{0, \dots, k\}\) sends each \(i < k\) to \(\varphi(i)\) and sends \(k\) to \(p\).

def extendMap {N k : ℕ} (φ : Fin k → Fin N) (p : Fin N) : Fin (k + 1) → Fin N :=
  fun i => if h : i.val < k then φ ⟨i.val, h⟩ else p
Used by 4
Used byExtending a decreasing subsequence · Appending a later index keeps indices increasing · The last entry of an appended map · Extending an increasing subsequence

TheoremEntries of a strictly increasing index map lie at or below its last entry#✓fully proved

Let \(k \ge 1\) and let \(\varphi : \{0, \dots, k-1\} \to \{0, \dots, N-1\}\) be strictly increasing with \(\varphi(k-1) = q\). Then \(\varphi(i) \le q\) for every \(i < k\).

theorem idx_le_last {N k : ℕ} {q : Fin N} {φ : Fin k → Fin N}
    (hk : 0 < k) (hidx : ∀ i j : Fin k, i < j → φ i < φ j)
    (hlast : φ ⟨k - 1, sub_one_lt_of_pos hk⟩ = q)
    {i : Fin (k + 1)} (hik : i.val < k) :
    φ ⟨i.val, hik⟩ ≤ q
Uses 1 · Used by 2
Statement usesA positive natural number exceeds its predecessor
Used byAppending a later index keeps indices increasing · Extending an increasing subsequence

TheoremThe last value is the largest along a strictly increasing selection#✓fully proved

Let \(f\) be a real sequence indexed by \(\{0, \dots, N-1\}\), let \(k \ge 1\), and let \(\varphi\) map \(\{0, \dots, k-1\}\) to \(\{0, \dots, N-1\}\) so that \(f(\varphi(i)) < f(\varphi(j))\) whenever \(i < j < k\). If \(\varphi(k-1) = q\), then \(f(\varphi(i)) \le f(q)\) for every \(i < k\).

theorem val_le_last_incr {N k : ℕ} {f : Fin N → ℝ} {q : Fin N}
    {φ : Fin k → Fin N} (hk : 0 < k)
    (hval : ∀ i j : Fin k, i < j → f (φ i) < f (φ j))
    (hlast : φ ⟨k - 1, sub_one_lt_of_pos hk⟩ = q)
    {i : Fin (k + 1)} (hik : i.val < k) :
    f (φ ⟨i.val, hik⟩) ≤ f q
Uses 1 · Used by 1
Statement usesA positive natural number exceeds its predecessor
Used byExtending an increasing subsequence

TheoremThe last value is the smallest along a strictly decreasing selection#✓fully proved

Let \(f\) be a real sequence indexed by \(\{0, \dots, N-1\}\), let \(k \ge 1\), and let \(\varphi\) map \(\{0, \dots, k-1\}\) to \(\{0, \dots, N-1\}\) so that \(f(\varphi(j)) < f(\varphi(i))\) whenever \(i < j < k\). If \(\varphi(k-1) = q\), then \(f(q) \le f(\varphi(i))\) for every \(i < k\).

theorem last_le_val_decr {N k : ℕ} {f : Fin N → ℝ} {q : Fin N}
    {φ : Fin k → Fin N} (hk : 0 < k)
    (hval : ∀ i j : Fin k, i < j → f (φ j) < f (φ i))
    (hlast : φ ⟨k - 1, sub_one_lt_of_pos hk⟩ = q)
    {i : Fin (k + 1)} (hik : i.val < k) :
    f q ≤ f (φ ⟨i.val, hik⟩)
Uses 1 · Used by 1
Statement usesA positive natural number exceeds its predecessor
Used byExtending a decreasing subsequence

TheoremAppending a later index keeps indices increasing#✓fully proved

Let \(k \ge 1\) and let \(\varphi : \{0, \dots, k-1\} \to \{0, \dots, N-1\}\) be strictly increasing with last value \(\varphi(k-1) = q\). If \(p\) is an index with \(q < p\), then the map on \(\{0, \dots, k\}\) obtained by appending \(p\) to \(\varphi\), which sends each \(i < k\) to \(\varphi(i)\) and sends \(k\) to \(p\), is strictly increasing.

theorem extend_idx {N k : ℕ} {q p : Fin N} {φ : Fin k → Fin N}
    (hk : 0 < k) (hidx : ∀ i j : Fin k, i < j → φ i < φ j)
    (hlast : φ ⟨k - 1, sub_one_lt_of_pos hk⟩ = q) (hqp : q < p)
    (i j : Fin (k + 1)) (hij : i < j) :
    extendMap φ p i < extendMap φ p j
Uses 3 · Used by 1
Statement usesAppending an entry to a map of indices · A positive natural number exceeds its predecessor
Proof usesEntries of a strictly increasing index map lie at or below its last entry
Used byExtending a decreasing subsequence

TheoremThe last entry of an appended map#✓fully proved

For every map \(\varphi : \{0, \dots, k-1\} \to \{0, \dots, N-1\}\) and every \(p \in \{0, \dots, N-1\}\), the map obtained by appending \(p\) to \(\varphi\) takes the value \(p\) at its last index \(k\).

theorem extend_last {N k : ℕ} (φ : Fin k → Fin N) {p : Fin N}
    (hk1 : 0 < k + 1) :
    extendMap φ p ⟨k + 1 - 1, sub_one_lt_of_pos hk1⟩ = p
Uses 2 · Used by 2
Statement usesAppending an entry to a map of indices · A positive natural number exceeds its predecessor
Used byExtending a decreasing subsequence · Extending an increasing subsequence

TheoremExtending an increasing subsequence#✓fully proved

Let \(f : \{0, \dots, N-1\} \to \mathbb{R}\), let \(k \ge 1\), and let \(\varphi\) be an increasing subsequence of \(f\) of length \(k\) (indices and values strictly increasing) with last index \(\varphi(k-1) = q\). If \(p \in \{0, \dots, N-1\}\) satisfies \(q < p\) and \(f(q) < f(p)\), then \(f\) has an increasing subsequence of length \(k + 1\) ending at \(p\).

theorem incrExtend {N k : ℕ} {f : Fin N → ℝ} {q p : Fin N} {φ : Fin k → Fin N}
    (hk : 0 < k) (hsub : IsIncrSubseq f k φ)
    (hlast : φ ⟨k - 1, sub_one_lt_of_pos hk⟩ = q)
    (hqp : q < p) (hval : f q < f p) : IsIncrEnd f p (k + 1)
Uses 7 · Used by 1
Statement usesIncreasing subsequence ending at a position · Increasing subsequence · A positive natural number exceeds its predecessor
Proof usesAppending an entry to a map of indices · The last entry of an appended map · Entries of a strictly increasing index map lie at or below its last entry · The last value is the largest along a strictly increasing selection
Used byLongest increasing subsequence lengths increase strictly along increasing pairs

TheoremExtending a decreasing subsequence#✓fully proved

Let \(f\) be a real sequence indexed by \(\{0, \dots, N-1\}\), let \(k \ge 1\), and let \(\varphi\) be a decreasing subsequence of \(f\) of length \(k\), that is, indices \(\varphi(0) < \dots < \varphi(k-1)\) with \(f(\varphi(0)) > \dots > f(\varphi(k-1))\), whose last index is \(\varphi(k-1) = q\). If \(p\) is an index with \(q < p\) and \(f(p) < f(q)\), then \(f\) has a decreasing subsequence of length \(k + 1\) that ends at \(p\).

theorem decrExtend {N k : ℕ} {f : Fin N → ℝ} {q p : Fin N} {φ : Fin k → Fin N}
    (hk : 0 < k) (hsub : IsDecrSubseq f k φ)
    (hlast : φ ⟨k - 1, sub_one_lt_of_pos hk⟩ = q)
    (hqp : q < p) (hval : f p < f q) : IsDecrEnd f p (k + 1)
Uses 7 · Used by 1
Statement usesDecreasing subsequence ending at a position · Decreasing subsequence · A positive natural number exceeds its predecessor
Proof usesAppending an entry to a map of indices · Appending a later index keeps indices increasing · The last entry of an appended map · The last value is the smallest along a strictly decreasing selection
Used byLongest decreasing subsequence lengths grow along a descent

TheoremLongest increasing subsequence lengths increase strictly along increasing pairs#✓fully proved

Let \(f : \{0, \dots, N-1\} \to \mathbb{R}\) and let \(q < p\) be positions with \(f(q) < f(p)\). Then the length of the longest increasing subsequence of \(f\) ending at \(q\) is strictly less than the length of the longest increasing subsequence of \(f\) ending at \(p\).

theorem incrMono {N : ℕ} (f : Fin N → ℝ) {q p : Fin N}
    (hqp : q < p) (hval : f q < f p) : incrLen f q < incrLen f p
Uses 7 · Used by 1
Statement usesLength of the longest increasing subsequence ending at a position
Proof usesIncreasing subsequence ending at a position · Increasing subsequence · Extending an increasing subsequence · The longest increasing subsequence ending at a position is attained · Bound by the longest increasing subsequence ending at a position · A positive natural number exceeds its predecessor
Used byErdős–Szekeres theorem

TheoremLongest decreasing subsequence lengths grow along a descent#✓fully proved

Let \(f\) be a real sequence indexed by \(\{0, \dots, N-1\}\), and let \(q < p\) be indices with \(f(p) < f(q)\). Then the length of the longest strictly decreasing subsequence of \(f\) ending at \(q\) is strictly less than the length of the longest strictly decreasing subsequence of \(f\) ending at \(p\).

theorem decrMono {N : ℕ} (f : Fin N → ℝ) {q p : Fin N}
    (hqp : q < p) (hval : f p < f q) : decrLen f q < decrLen f p
Uses 7 · Used by 1
Statement usesLength of the longest decreasing subsequence ending at a point
Proof usesDecreasing subsequence ending at a position · Decreasing subsequence · Extending a decreasing subsequence · The longest decreasing subsequence ending at a point is attained · Bound by the longest decreasing subsequence ending at a position · A positive natural number exceeds its predecessor
Used byErdős–Szekeres theorem

TheoremIncreasing subsequences of every smaller length#✓fully proved

Let \(f\) be a real sequence indexed by \(\{0, \dots, N-1\}\). If \(f\) has a strictly increasing subsequence of length \(k\), then for every \(r \le k\) it has a strictly increasing subsequence of length \(r\).

theorem truncIncr {N k r : ℕ} {f : Fin N → ℝ} {φ : Fin k → Fin N}
    (hsub : IsIncrSubseq f k φ) (hrk : r ≤ k) :
    ∃ φ' : Fin r → Fin N, IsIncrSubseq f r φ'
Uses 1 · Used by 1
Statement usesIncreasing subsequence
Used byErdős–Szekeres theorem

TheoremDecreasing subsequences of every smaller length#✓fully proved

Let \(f\) be a real sequence indexed by \(\{0, \dots, N-1\}\). If \(f\) has a strictly decreasing subsequence of length \(k\), then for every \(s \le k\) it has a strictly decreasing subsequence of length \(s\).

theorem truncDecr {N k s : ℕ} {f : Fin N → ℝ} {φ : Fin k → Fin N}
    (hsub : IsDecrSubseq f k φ) (hsk : s ≤ k) :
    ∃ ψ : Fin s → Fin N, IsDecrSubseq f s ψ
Uses 1 · Used by 1
Statement usesDecreasing subsequence
Used byErdős–Szekeres theorem

TheoremErdős–Szekeres theorem#✓fully proved

Let \(r, s \ge 1\) be natural numbers, let \(N = (r - 1)(s - 1) + 1\), and let \(f\) be an injective real sequence indexed by \(\{0, \dots, N-1\}\). Then \(f\) has a strictly increasing subsequence of length \(r\), that is, indices \(i_1 < \dots < i_r\) with \(f(i_1) < \dots < f(i_r)\), or a strictly decreasing subsequence of length \(s\), that is, indices \(j_1 < \dots < j_s\) with \(f(j_1) > \dots > f(j_s)\).

public theorem erdos_szekeres {r s : ℕ} (hr : 0 < r) (hs : 0 < s)
    (f : Fin ((r - 1) * (s - 1) + 1) → ℝ) (hinj : Function.Injective f) :
    (∃ φ : Fin r → Fin ((r - 1) * (s - 1) + 1),
      (∀ i j : Fin r, i < j → φ i < φ j) ∧
      (∀ i j : Fin r, i < j → f (φ i) < f (φ j))) ∨
    (∃ ψ : Fin s → Fin ((r - 1) * (s - 1) + 1),
      (∀ i j : Fin s, i < j → ψ i < ψ j) ∧
      (∀ i j : Fin s, i < j → f (ψ j) < f (ψ i)))
Uses 16
Proof usesDecreasing subsequence ending at a position · Decreasing subsequence · Increasing subsequence ending at a position · Increasing subsequence · Length of the longest decreasing subsequence ending at a point · The longest decreasing subsequence ending at a point has length at least one · The longest decreasing subsequence ending at a point is attained · Longest decreasing subsequence lengths grow along a descent · No strict pair in a one-element set · Length of the longest increasing subsequence ending at a position · Longest increasing subsequences ending at a position have length at least one · The longest increasing subsequence ending at a position is attained · Longest increasing subsequence lengths increase strictly along increasing pairs · A positive natural number exceeds its predecessor · Decreasing subsequences of every smaller length · Increasing subsequences of every smaller length
30 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.