Erdős–Szekeres theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves Theorem 73 from the 100 Theorems List, also known as the Erdős–Szekeres theorem: given a sequence of more than r * s distinct values, there is an increasing sequence of length longer than r or a decreasing sequence of length longer than s.

We use the proof outlined at https://en.wikipedia.org/wiki/Erdos-Szekeres_theorem#Pigeonhole_principle.

Tags #

sequences, increasing, decreasing, Ramsey, Erdos-Szekeres, Erdős–Szekeres, Erdős-Szekeres

source

theorem theorems_100.erdos_szekeres {α : Type u_1} [linear_order α] {r s n : ℕ} {f : fin n → α} (hn : r * s < n) (hf : function.injective f) :

(∃ (t : finset (fin n)), r < t.card ∧ strict_mono_on f ↑t) ∨ ∃ (t : finset (fin n)), s < t.card ∧ strict_anti_on f ↑t

Erdős–Szekeres Theorem: Given a sequence of more than r * s distinct values, there is an increasing sequence of length longer than r or a decreasing sequence of length longer than s.

Proof idea: We label each value in the sequence with two numbers specifying the longest increasing subsequence ending there, and the longest decreasing subsequence ending there. We then show the pair of labels must be unique. Now if there is no increasing sequence longer than r and no decreasing sequence longer than s, then there are at most r * s possible labels, which is a contradiction if there are more than r * s elements.