Strict positivity of a nonzero mixed matrix integral
ProvedRybinAI2026.P01.crossIntegral_posintegral-inequalitymatrix-analysispositive-definite-matrices
Let be distinct real matrices and let be real symmetric positive-definite matrices. Then the mixed spherical integral with numerator and denominator is strictly positive:
No separate positive-dimension assumption is needed: the existence of two distinct matrices indexed by already excludes the zero-dimensional case. This lemma permits cancellation of positive cross-integral factors in denominator-normalization arguments.
Preamble
import Definitions.Def_rybin2026_p01_cross_integral open Matrix RybinAI2026.P01
Formal statement
theorem RybinAI2026.P01.crossIntegral_pos {n : ℕ}
(X Y P Q : Matrix (Fin n) (Fin n) ℝ)
(hXY : X ≠ Y) (hP : P.PosDef) (hQ : Q.PosDef) :
0 < crossIntegral X Y P Q := by
sorry
Source