> [!NOTE] Theorem (Lower bound for Longest Monotonic Subsequence)
> Every [[List|list]] $a_{1},\dots,a_{n^{2}+1}$ of distinct real numbers contains a [[Monotonic Sequence of Real Numbers|monotonic]] [[Real Subsequence|subsequence]] of length $n+1$.
>*Proof*. For $k\in [n^{2}+1]$, let $f(k)$ denote the length of the longest increasing subsequence starting at $a_{k}$. Observe that $f(k) \geq 1$ for every $k\in[n^{2}+1]$.
>
>Moreover, if $f(k)\geq n+1$ for some $k\in[n^2+1]$ then we are done because we have identified an increasing subsequence of length $n+1$.
>
>Otherwise, $f(k)\leq n$ for every $k\in[n^{2}+1]$. By [[Pigeonhole Principle#^d018fb|pigeonhole principle]], there exists $l\in [n]$ such that $|f^{-1}(l)|\geq n+1$.
>
>Noting that they're a distinct, let $i_{1}<\dots i_{n+1}$ such that $f(i_{1})=\dots=f(i_{n+1})=l$.
>We claim that $a_{i_{1}},a_{i_{2}},\dots,a_{i_{n+1}}$ forms a decreasing subsequence. Suppose that this is not the case and let $j,j'\in[n+1]$ such that $i_{j}<i_{j'}$ and $a_{i_{j}}<a_{i_{j'}}$.
>However, in this case $f(i_{j})$ would be strictly greater than $f(i_{j'})$ which contradicts $f(i_{j})=f(i_{j'})$. $\square$
> [!NOTE] Theorem (Erdös-Szekeres)
> Every finite sequence $a_{1},\dots,a_{(r-1)(s-1)+1}$ of distinct real numbers contains either an increasing subsequence of length $r$ or a decreasing subsequence of length $s$.
>*Proof*. For every $k\in[(r-1)(s-1)+1]$, let $f(k)$ denote the the longest increasing subsequence starting at $a_{k}$.
>
>If $f(k)=r$ for some $k\in[(r-1)(s-1)+1]$ then we are done.
>
>Otherwise, suppose $f(k) <r$ for all $k\in[(r-1)(s-1)+1]$. By *pigeonhole principle*, there exists $l\in[(r-1)(s-1)+1]$ such that $|f^{-1}(l)|\geq s$.
>Let $i_{1}<\dots<i_{s}$ such that $f(i_{1})=\dots=f(i_{s})=l$. We claim that $a_{i_{1}},\dots a_{i_{s}}$ is decreasing. Suppose to the contrary that there exists $j,j'\in[s]$ such that $i_{j}<i_{j'}$ and $a_{i_{j}}<a_{i_{j'}}$ then $f(i_{j})>f(i_{j'})$ which contradicts the fact that $f(i_{j}=i_{j'})$. $\square$
# Applications
- [[Longest Increasing Subsequence]].