Numerator subadditivity of $\operatorname{crossIntegral}$

Numerator subadditivity for the mixed spherical integral.

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

The left-hand side equals $d(A+B,C+D)$. On the right the numerator difference $(A+B)-(C+D)$ has been split as $(A-C)+(B-D)$, while the denominator $\bigl(u^{\mathsf T}(A+B)u\bigr)\bigl(v^{\mathsf T}(C+D)v\bigr)$ is left unchanged in both terms.

This is the elementary first half of the additive Problem 1 inequality. It holds pointwise on $S^{n-1}\times S^{n-1}$ from the identity $(A+B)-(C+D)=(A-C)+(B-D)$ and the scalar triangle inequality $|x+y|\le|x|+|y|$, together with strict positivity of the shared denominator on positive-definite inputs and integrability of the three kernels on the compact product of spheres.

Formalization Note crossIntegral and distance are from the Problem 1 definition modules; the four positive-definiteness hypotheses guarantee the denominator quadratic forms are strictly positive on the sphere.