Matrix integral inequality under uniform relative quadratic-form bounds

Let $n$ be a natural number and let $A,B,C,D$ be real symmetric positive-definite $n\times n$ matrices. Let $d$ be the original double spherical integral from Problem 1, with unnormalized surface measure. Suppose positive real constants $l,U,m,V$ satisfy the Loewner comparisons

and the coefficient budget

Then

Here $H\preceq K$ means that $K-H$ is positive semidefinite. The comparisons give uniform lower and upper bounds on the relative quadratic forms $u^{\mathsf T}Bu/u^{\mathsf T}Au$ and $v^{\mathsf T}Dv/v^{\mathsf T}Cv$. This sufficient condition is a restricted case of Problem 1 and does not assert the unrestricted inequality. It contains the scalar-threshold regime when sharp relative bounds are used, and also covers examples with overlapping relative spectral intervals and noncollinear differences. Dimension zero is included formally; its sphere is empty and its distances vanish.

Formalization Note Positive definiteness is Mathlib's Matrix.PosDef, which includes Hermitian symmetry. The four comparisons are represented by Matrix.PosSemidef of matrix differences; the original integral definitions are unchanged.