Mixed integrals sum to at most $\max\{d(A,C),d(B,D)\}$

Denominator-normalisation bound: the two mixed integrals sum to at most the larger distance.

Let $n>0$ and let $A,B,C,D$ be real symmetric positive-definite $n\times n$ matrices. Write $\operatorname{crossIntegral}$ for the mixed spherical integral and $d(\cdot,\cdot)$ for the CUHK-Shenzhen Problem 1 distance. Then

Each summand is obtained from a Problem 1 distance by inflating its denominator from the diagonal pair to $\bigl(u^{\mathsf T}(A+B)u\bigr)\bigl(v^{\mathsf T}(C+D)v\bigr)$; individually one has $\operatorname{crossIntegral}(A,C,A+B,C+D)\le d(A,C)$ and $\operatorname{crossIntegral}(B,D,A+B,C+D)\le d(B,D)$. The content of the statement is that after this inflation the two terms together are bounded by the maximum of the two distances, not merely by their sum.

Together with numerator subadditivity this yields the additive Problem 1 inequality $d(A+B,C+D)\le\max\{d(A,C),d(B,D)\}$ for arbitrary positive-definite $A,B,C,D$. Writing $K_A,K_B$ for the two summands and $I_A=d(A,C)$, $I_B=d(B,D)$, the bound is equivalent to $K_A/I_A+K_B/I_B\le 1$ when $I_A,I_B>0$; the degenerate cases $A=C$ or $B=D$ hold directly because the corresponding numerator vanishes identically.

Formalization Note crossIntegral and distance are from the Problem 1 definition modules. The bound is uniform in the dimension $n>0$.