I found this little gem in an old post on Terry Tao’s blog. There’s not really enough content in it to merit an entire Extremal Toolbox post, but it’s too cool not to point out.

**Theorem**. Graphs of order and girth at least 5 have edges.

**Proof**. Suppose that has edges. Define the function to be the “adjacency characteristic function.” Now, by Cauchy-Schwarz:

.

Clearly for fixed, is unbounded as . But the first expression is times the number of (possibly degenerate) 4-cycles in the graph; it’s easy to check that there are degenerate 4-cycles, so as n is unbounded our graph must contain a 4-cycle. QED

Now, it’s possible to get better bounds by cleverly doing “surgery” on the graph and just using pigeonhole. (See here for details.) But it’s tricky and far less beautiful than the argument with Cauchy-Schwarz, which really demonstrates one way in which C-S can be thought of as “strengthening” pigeonhole.