An aside about ${+1,-1}$ sequences: how to prove adequately? I was listening to Tao's lecture on the Erdos Discrepancy Problem, which asks if
$\left|\sum _{{i=1}}^{k}x_{{i\cdot d}}\right|$ is unbounded for each sequence $x_n\in\{-1,+1\}$. That statement, he said, was equivalent to the existence of $N(C)$ (dependent only on $C$), such that one of the sums $|x_d+x_{2d}+...+x_{kd}|>C$, with $kd\leq N(C)$, regardless of the choice of $\{x_i\}$.
A question came to mind: why is it impossible to find sequences for which discrepancy needs larger and larger $N$, even with the same $C$? Would that contradict Erdos's conjecture?
Eventually I found this idea: if you interpret $-1$ as $0$, the sequences are the binary representation of $\{0\leq x\leq1\}$. Fix $C$. Now the set $S_n$ of sequences for which $N>n$ is a closed set in $\mathbb{R}$. This is because a sequence is in $S_n$ if and only if the first $n$ terms are so-and-so; the other terms do not matter. Therefore $S_n$ is made up of finitely many closed intervals of the form $[x, x+2^{-n}]$ where $x=2^{-1}a_1+...+2^{-n}a_n$. Since $S_n\subset S_{n+1}$, the intersection of all these closed $S_n$ is a non-empty set, giving the fictitious counterexample to the Problem.
But I do not like this approach. Real analysis seems to be overkill for a statement about arithmetic. How else can I formalise the above idea?
 A: You can also prove such a statement by König's lemma (Wikipedia link).
A sequence for which $N>n$ is equivalent to a finite sequence of length $n$ with discrepancy at most $C$. (By taking its first $n$ terms.) So construct the tree $T$ made up of finite sequences of discrepancy at most $C$. We put an edge from $(x_1, x_2, \dots, x_n)$ to $(x_1, x_2, \dots, x_n, x_{n+1})$ whenever both of these sequences have discrepancy at most $C$: that is, edges represent extending the sequence by one element.
If arbitrarily long finite sequences exist, then in particular infinitely many exist (in fact, one is equivalent to the other). So the tree $T$ is infinite; but all degrees are finite. By König's lemma, we can find an infinite branch of the tree, which corresponds to an infinitely long sequence with discrepancy at most $C$.

I should also mention that (a more general version of) your argument is a very common idea in combinatorics: so common that it tends to get skipped over in proofs and summarised by the clause "By the standard compactness argument, ..."
Rather than interpret binary sequences as elements of $\mathbb R$, we can work directly over $\{-1,+1\}^\infty$. This is a compact space by Tychonoff's theorem (Wikipedia link), for instance - it is a product of discrete, and therefore compact, spaces. Here, the sets $S_n$ are all closed, so if we assume that $S_n \ne \varnothing$ for all $n$, then $\bigcap_{n=1}^\infty S_n \ne \varnothing$ by compactness, and so an infinite sequence with bounded discrepancy must exist.
In general, it appears that we do need some appeal to the axiom of choice to go from a statement about finite sequences (or the finite beginnings of infinite sequences) to the existence of an infinite sequence. (König's lemma requires some form of dependent choice to hold; Tychonoff's theorem is equivalent to the axiom of choice.) So I would not say that real analysis is "overkill".
