Cauchy–Schwarz

Finally I understand the Cauchy–Schwarz inequality! No induction needed.

Theorem
\(a, b\in \mathrm{Rat}^n\)
\(n\in\mathrm{Nat}\)
                     
\((a\bullet b)^2 \leq \mathop{\rm Q}(a)\mathop{\rm Q}(b)\)

Proof
Recall that by definition
\[a\bullet b=\sum_{i=1}^n a_ib_i\]\[\mathop{\rm Q}(a)=\sum_{i=1}^n a_i^2\]\[\mathop{\rm Q}(b)=\sum_{i=1}^n b_i^2.\]
The claim, reformulated as
\[\left(\sum_{i=1}^n a_ib_i\right)^2 \leq \left(\sum_{i=1}^n a_i^2\right)\left(\sum_{i=1}^n b_i^2\right),\]
is equivalent to (by distributing terms)
\[\left(\sum_{i=1}^n a_i^2b_i^2\right)+\sum_{1\leq i<j\leq n}2a_ib_ia_jb_j \leq \left(\sum_{i=1}^n a_i^2b_i^2\right)+\sum_{1\leq i<j\leq n}a_i^2b_j^2+a_j^2b_i^2\]
and (by collecting terms)
\[0 \leq \sum_{1\leq i<j\leq n}a_i^2b_j^2+a_j^2b_i^2-2a_ib_ia_jb_j = \sum_{1\leq i<j\leq n}(a_ib_j-a_jb_i)^2.\]
The last statement is true because squares are positive and sums of positive numbers are positive.