theorem
determinantal_conjecture
(n : Type)
[Fintype n]
[DecidableEq n]
(d1 d2 : n → ℂ)
(U1 U2 : ↥(unitary (Matrix n n ℂ)))
:
Does the determinant of the sum $A + B$ of two $n \times n$ normal complex matrices A and B always lie in the convex hull of the $n!$ points $\prod i (\lambda(A)_i + \lambda(B)_{σ(i)})$? Here the numbers $\lambda (A)_i$ and $\lambda (B)_i$ are the eigenvalues of $A$ and $B$, and $\sigma$ is an element of the symmetric group $S_n$.