Show $\sum\limits_{i=1}^n \sum\limits_{j=1}^n \cos(x_i - x_j) \geq 0$ for all real sequences $(x_i)_{1\leq i\leq n}$

Question

This inequality must be well known, and possibly easy to prove but I could not find it in the literature or here.

Does anyone have a proof of $$ \forall n\in \mathbb{N}^*, \forall x_k \in \mathbb{R}, \sum\limits_{i=1}^n \sum\limits_{j=1}^n \cos(x_i - x_j) \geq 0. $$ P.S.: The cases $n=2$ and $x_1=0$, $x_2 = \pi$, or the case $n=4$ and $x_k= \frac{k-1}{2}\pi$, etc... show that the inequality is sharp.

Answer 1

Note that $\cos(x)=\operatorname{Re}e^{ix}$. So, $$\sum_{i=1}^n\sum_{j=1}^n\cos(x_i-x_j)=\operatorname{Re}\sum_{i=1}^n\sum_{j=1}^n e^{i(x_i-x_j)}.$$ This sum can be factored as $$\sum_{i=1}^ne^{ix_i}\sum_{j=1}^ne^{-ix_j}=z\overline z,$$ where $z=\sum e^{ix_j}$ is a complex number. Since $z\overline z$ is a nonnegative real, its real part is positive, as desired.

Answer 2

Let's think about a different problem. Suppose $\hat{e}_1 , \ldots, \hat{e}_n$ are unit vectors. Then for each $\hat{e}_j$ there exists $\theta_j \in [0, 2\pi)$ such that $\hat{e}_j = \cos\theta_j \hat{x} + \sin\theta_j \hat{y}$. Then $$ \hat{e}_i \cdot \hat{e}_j = \cos\theta_i \cos\theta_j + \sin\theta_i \sin\theta_j = \cos(\theta_i - \theta_j) $$ Then $$ \sum_i \sum_j \cos(\theta_i - \theta_j) = \sum_i \sum_j \hat{e}_i \cdot \hat{e}_j = \sum_i \hat{e}_i \cdot \sum_j \hat{e}_j $$ Set $\vec{v} = \sum_i \hat{e}_i$. Then $$ \sum_i \sum_j \cos(\theta_i - \theta_j) = \vec{v} \cdot \vec{v} \geq 0 $$ To see how this problem is equivalent to your problem, observe that we may reduce each $x_i$ mod $2\pi$ WLOG (why?).

Answer 3

The identity $\cos(x_i - x_j) = \cos(x_i)\cos(x_j) + \sin(x_i)\sin(x_j)$ implies $$\sum_{i,j} \cos(x_i - x_j) = \bigg(\sum_i \cos(x_i)\bigg)^2 + \bigg(\sum_i \sin(x_i)\bigg)^2 \ge 0.$$