an optimization problem

Stream: maths

[Alex Zhang]

Given an arbitrary square matrix with the row sum of each row fixed. Could anyone explain or hint how to rigorous establish that a matrix with pairwisely perpendicular rows (properly ordered) is an optimal solution to the determinant optimization problem?

[Yaël Dillies]

It might be related to the Birkhoff-Von Neumann problem? If the determinant is convex in any useful way (not sure convexity even makes sense), then you know it's maximized on doubly stochastic matrices (which what you asked for, unless you're allowed negative coefficients?) by an extreme point, which is a permutation matrix thanks to Birkhoff-Von Neumann.

[Yaël Dillies]

I just made all of that up so don't take my word for it.

[David Wärn]

I think what you really want is to fix the sum-of-squares in each row? For positive entries you can relate this to the sum via $\sum_i x_i^2 \le (\sum x_i)^2$, but otherwise you get very large determinant from for example $\begin{pmatrix} 1 & 0 \\ -100 & 101 \end{pmatrix}$.

[David Wärn]

I guess if you have an inner product space $V$, there's a well-behaved notion of the $k$-volume $M(v_1 \ldots v_k)$ spanned by $k$ vectors $v_1 \ldots v_k$ (say, pick an orthonormal basis of the subspace spanned by them, and look at the absolute value of the determinant of the corresponding $k \times k$-matrix). For $k = \dim V$ this gives you the determinant. And you should be able to prove a bound $M(v_1 \ldots v_k) \le \prod_i \lVert v_i \rVert$ by induction on $k$, using a generalization of the "base times height" formula for the area of a parallelogram.

[Alex Zhang]

Yes. fix the sum-of-squares

[Alex Zhang]

what is the generalization of the "base times height" formula?

[David Wärn]

By using Laplace expansion in a suitable basis, you should be able to show that $M(v_1 \ldots v_{k+1}) = M(v_1 \ldots v_k) \lVert v_{k+1} - u \rVert$, where $u$ is the projection of $v_{k+1}$ onto the subspace spanned by $v_1 \ldots v_k$

[David Wärn]

Btw I have no idea what would be the best way to formalize this result in mathlib

[Alex Zhang]

This seems like a reasonable way to formally prove the result, but I feel it can be tedious to encode it.

[Kyle Miller]

This seems like a job for Lagrange multipliers and Jacobi's formula. A sketch:

First, consider the submanifold of $k\times k$ matrices where row $i$ has length $c_i$, with $c_1,\dots,c_k>0$. This submanifold is a level set of $A\mapsto (\lVert v_1\rVert,\dots,\lVert v_k\rVert)$ for the codomain point $(c_1,\dots,c_k)$, and let $A$ denote a matrix in this submanifold. Let $A_i$ denote the matrix $A$, but setting all but row $i$ to $0$. The matrices $A_1,\dots,A_k$ span the subspace of the tangent bundle that are orthogonal to the submanifold at $A$.

One version of Jacobi's formula is that $\partial\det(A)/\partial{A_{ij}} = \operatorname{adj}(A)_{ji}$, where $A_{ij}$ is entry $(i,j)$ of $A$. A critical point of $\det$ when restricted to the submanifold corresponds to a matrix $A$ where the matrix $(\partial\det(A)/\partial{A_{ij}})_{ij}$ lies in the subspace spanned by $A_1,\dots,A_k$, thus we can say each column of $\operatorname{adj}(A)$ is a scalar multiple of the corresponding row of $A$.

Assuming $\det(A)\neq 0$, then $A$ is invertible, so $\operatorname{adj}(A)=\det(A)A^{-1}$. Since $AA^{-1}=I$, putting this all together the rows of $A$ are pairwise perpendicular. We can ignore $\det(A)=0$ as an optimum since the diagonal matrix with $c_1,\dots,c_n$ on the diagonal gives a lower bound for the maximal determinant.

[David Wärn]

You can rephrase my argument above to make it more direct: if $A$ is a square matrix, then you should be able to show that there exists a unitary matrix $U$ such that $AU$ is upper triangular. This has the same (absolute value of) determinant as $A$, and the norms of the rows are the same. But now the conclusion is clear, since the determinant is a product of diagonal entries, and the norms are lower bounded by diagonal entries.

[Will Sawin]

I think this is called Hadamard's inequality and searching that should give a proof.

[Dima Pasechnik]

yes, and in fact a student of mine worked on formalising Hadamard matrices in Liean+mathlib last summer.

[Dima Pasechnik]

And this student is @Alex Zhang (hi!) - whom I only recognised from the email :-)

[Dima Pasechnik]

Hadamard matrices are ones for which Hadamard inequality turns into equation (one can renormalise the nxn matrix to have its rows and columns to be of squared Euclidean norm n, and entries have norm at most 1 (and thus exactly 1).

[Alex Zhang]

Hi, Dima! @Dima Pasechnik