Eigenvalues of products of exponential families

I have a question about a close cousin of the multiplicative eigenvalue problem.

Let $ U$ be a special unitary matrix with diagonalization $ D = \operatorname{diag}(e^{2 \pi i a_1}, \ldots, e^{2 \pi i a_n})$ . The $ a_j$ may be normalized so as to satisfy $ a_1 \le a_2 \le \cdots \le a_n \le a_1 + 1$ and $ a_1 + \cdots + a_n = 0$ . These extra conditions have the advantage of producing a canonical sequence of logarithms: we may define a function $ \operatorname{LogSpec}$ by $ $ \operatorname{LogSpec} U = (a_1, \ldots, a_n).$ $

It also has the disadvantage of being not smooth. Given a point in $ \mathbb R^n$ satisfying only the equality $ a_1 + \cdots + a_n = k$ for $ k \in \mathbb{Z}$ , this point can be moved into by the region satisfying the family of inequalities (without modifying its image through $ t \mapsto e^{2 \pi i t}$ ) by repeated reflection. Let’s call this assignment $ R$ , as in $ $ R\colon\thinspace \left\{ a_* \in \mathbb R^n \mid a_1 + \cdots + a_n = 0\right\} \to \left\{a_* \in \mathbb R^n \middle| \begin{array}{c} a_1 + \cdots + a_n = 0, \ a_j \le a_{j+1}, \; a_n \le a_1 + 1 \end{array} \right\}.$ $ By consequence, curves like $ $ \gamma(t) = \operatorname{LogSpec} \exp\left(\begin{array}{cccc} it & 0 \ 0 & -it \end{array}\right),$ $ which are smooth in $ SU(2)$ before postcomposition with $ \operatorname{LogSpec}$ , become a kind of sawtooth function. For ease of reference below, I’ll call the image of a convex set through $ R$ folded-convex.

Question: I would like to know a reference for (or, indeed, a proof of) the following result:

$ \DeclareMathOperator{\LogSpec}{LogSpec}$ ??Theorem??: Let $ \xi_1, \ldots, \xi_m$ be a sequence of $ n \times n$ anti-Hermitian matrices, each exponentiating to a closed subgroup of $ U(n)$ . The assignment $ $ (t_1, \ldots, t_m) \mapsto \LogSpec \left( \prod_{j=1}^m \exp(\xi_j t_j) \right)$ $ sends convex sets in $ \mathbb R^m$ to folded-convex sets in $ \mathbb{R}^n$ .

In the classical version of the multiplicative eigenvalue problem, the set $ $ L_{m,n} = \left\{(\LogSpec U_j)_{j=1}^m \in \mathbb{R}^{n \cdot m} \middle| \begin{array}{c} \text{$ U_j$ unitary}, \ U_1 \cdots U_m = 1 \end{array}\right\} \subseteq \mathbb{R}^{n \cdot m}$ $ is shown to be convex by a clever application of symplectic reduction. The method of proof in Meinrenken and Woodward’s A symplectic proof of Verlinde factorization involves giving an explicit model for the moduli of flat connections on the trivial $ U(n)$ –bundle over a punctured Riemann sphere, then using its symplectic structure and a symplectic convexity theorem (suitably augmented to cope with loop groups) to deduce the convexity of $ L_{m,n}$ .

Their methods are especially well-suited to dealing with formulas like $ $ 1 = \operatorname{Ad}_{c_1}(t_1) \cdots \operatorname{Ad}_{c_m}(t_m),$ $ where $ t_j \in \mathfrak t_j \subseteq \mathfrak{su}(n)$ are anti-Hermitian diagonal and $ c_j \in SU(n)$ are special unitary. I’m new to this material and to symplectic geometry broadly, and so I’ve been unable to tweak these methods into saying something about this more restricted problem, where there are far fewer adjoint actions in play. Despite that, this seems like the kind of problem that would have attracted classical attention, and so I’m hopeful that there exists a resource that works this out. I’m also happy to hear about adjacent results—maybe I can make do with one of them.

Caveat lector: the theorem seems true in numerical experiment, but without a proof, there may well be edge cases unaccounted for. I’d be very, very happy to hear about those.