Let $A$ be a $k \times n$ orthogonal matrix; i.e., $AA^T = I\_{k \times k}$. For $1 \leq j \leq n$, let the squared norm of the $j$-th column of $A$ be denoted by $\alpha\_j^2$; i.e.,
$$\sum\_{i=1}^k a\_{ij}^2 = \alpha\_j^2.$$
Let $\Lambda = \operatorname{Diag}(\lambda\_1, \lambda\_2, \dotsc, \lambda\_n)$ be a positive definite matrix. Define a function $F$ from the space of p.d. diagonal matrices to $\mathbb R$ as follows:
$$ F(\Lambda) = \log \lvert A \Lambda A^T\rvert-\sum\_{j=1}^n \alpha\_j^2 \log \lambda\_j.$$


**To show**: $F(\Lambda) \geq 0$, with equality only when $\Lambda$ is a multiple of identity.


**Background**: This result is true and follows from an inequality known in information theory as Zamir and Feder's entropy power inequality. To obtain the result, we may apply Zamir and Feder's inequality to Gaussian random variables with covariances $\lambda\_i$. (A statement of the inequality may be found here: [Rioul - Information-theoretic proofs of entropy power inequalities](https://arxiv.org/abs/0704.1751), Proposition 9, (65c).)


I am interested in knowing if there is an alternate proof of this result that does not rely on entropy inequalities, and uses linear algebraic tools instead.



Matrix determinant inequality proof without using information theory
Here's a more general result. 


From [Choi's inequality](https://www.projecteuclid.org/download/pdf_1/euclid.ijm/1256051007), we know that for a positive linear map $\Phi$ and an operator convex function $f$, we have $\Phi(f(\Lambda)) \ge f (\Phi(\Lambda))$. Let $\Phi(\Lambda)=A\Lambda A^T$, and let $f(t)=-\log t$, then we obtain
\begin{align\*}
-A\log(\Lambda)A^T \ge -\log(A\Lambda A^T)\\
\Leftrightarrow\qquad\log(A\Lambda A^T) \ge A\log(\Lambda)A^T.
\end{align\*}
This operator inequality is stronger than the what we need. Simply take the trace of both sides to conclude $F(\Lambda) \ge 0$ (using the observation that $\log\det(Z)=\text{tr}\log Z$, and since $\Lambda$ is diagonal).


