Ask the validity of a scalar inequality  Let $a_i>0$, $x_i, y_i\in \mathbb{R}$ $i=1,\cdots, n$, such that 
$\sum\limits_{i=1}^nx_iy_i=0$,  $\sum\limits_{i=1}^nx_i^2=\sum\limits_{i=1}^ny_i^2=1$. Is it true $$
\left[\sum\limits_{i=1}^n\frac{1}{a_i}x_i^2\right] \left[\sum\limits_{1\le i < j \le n} a_ia_j(x_iy_j-x_jy_i)^2\right]\ge \sum\limits_{i=1}^n  a_i y_i^2?
$$
I tried the case $n=2$ and the special case where all $a_i$ are equal.
Motivation: To find a lower bound for difference in Lagrange identity under certain conditions. 
 A: The answer is yes.
Edit: As pointed out in the comment below, my first answer was not correct (it was proving the inequality with a factor 2). Here is the correction.  
Denote by $A$ the $n \times n$ matrix given by $A_{i,j} = \sqrt{ a_i a_j} (x_j y_i - x_i y_j)$, by $x'=(\sqrt{a_i^{-1}} x_i) \in \mathbb R^n$ and by $y'=(\sqrt{a_i} y_i) \in \mathbb R^n$. You are asking whether $|y'| \leq |x'| \| A\|_{HS}/{\sqrt 2}$. Here $|\cdot|$ denotes the usual euclidean norm on $\mathbb R^n$, and $\|\cdot\|_{HS}$ is the Hilbert-schmidt norm on matrices, ie $\|M\|_{HS} = \sqrt{Tr(M^*M)}$, where  $M^*$ is the (conjugate) transpose of $M$. 
By the assumptions $\langle x,y\rangle =0$ and $\langle x,x\rangle =1$, you have that $A x' = y'$. It is therefore enough to prove that $\|A\|_{op} \leq \|A\|_{HS}/\sqrt 2$, where $\|A\|_{op}$ is the operator norm acting on $\mathbb R^n$ with usual euclidean norm. But this holds because $A$ has real entries and is anti-hermitian, ie $A^* = -A$. If $\lambda$ is an eigenvalue of $A$, $\lambda \in i\mathbb R$ and $\bar \lambda$
 is also an eigenvalue of $A$. This proves the desired inequality, since $\|A\|_{op}$ is $\max_\lambda |\lambda|$ and $\|A\|_{HS} = (\sum_{\lambda} |\lambda|^2)^{1/2}$, where the max and the sum run over the eigenvalues of $A$ (counted with multiplicity).
