In my research, I encounter the following formula which I believe is correct (checked for $n\le3$). Is it classical ? If so, what is a reference ?


I am given a real symmetric matrix
$$S:=\int Y(t)Y(t)^Td\mu(t),$$
where $\mu$ is a probability and $Y(t):\Omega\rightarrow{\mathbb R}^n$.


Let $\sigma\_k(S)$ be the elementary symmetric polynomial in the eigenvalues of $S$. For instance, $\sigma\_1(S)$ is the trace and $\sigma\_n(S)$ the determinant. The following formula gives $\sigma\_k(S)$ in terms of the Gram matrix $G\_k(s\_1,\ldots,s\_k)$ whose entries are the scalar products $Y(s\_i)\cdot Y(s\_j)$.



> 
> $$\sigma\_k(S)=\frac1{k!}\int^{\otimes k}\det G\_k(s\_1,\ldots,s\_k)\,d\mu(s\_1)\cdots d\mu(s\_k).$$
> 
> 
> 


Remark that $S$ is positive semi-definite. The integrand is non-negative, as well as $\sigma\_k(S)$. The integrand vanishes identically iff $Y(t)$ takes values in a subspace of dimension $<k$, which is the condition under which $\sigma\_k(S)$ vanishes. It follows that, if the formula above failed, it would be because of an inequality between strictly positive numbers.


**Edit**. I delete the question mark in the formula above, because Marcel's answer and my comment to it, yield a proof.



A determinantal formula
The case $k=n$ is a consequence of the identity 


$$\int \det(f\_j(s\_k))\det(g\_j(s\_k))\prod\_{j=1}^N d\mu(s\_j) = N!\ \det\left(\int d\mu(t) f\_j(t)g\_k(t)\right)$$


which I have seen under the names "Andreief identity" and also "Gram identity". The proof is elementary using the Leibniz formula for the determinant.


