Mixed spherical integral $\operatorname{crossIntegral}(X,Y,P,Q)$

Definition

rybin2026_p01_cross_integral

by hnagoya · Sep 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

integral-inequalitymatrix-analysispositive-definite-matrices

Mixed spherical double integral for the CUHK-Shenzhen AI Math Problem 1 model.

For every dimension $n$ and arbitrary real $n\times n$ matrices $X,Y,P,Q$ , let $S^{n-1}\subset\mathbb R^n$ be the unit sphere carrying the surface measure $\sigma_n$ induced from Lebesgue measure by polar decomposition (no probability normalisation). Define

\operatorname{crossIntegral}(X,Y,P,Q)=\int_{S^{n-1}}\!\!\int_{S^{n-1}}\frac{\bigl|u^{\mathsf T}(X-Y)v\bigr|}{\bigl(u^{\mathsf T}Pu\bigr)\,\bigl(v^{\mathsf T}Qv\bigr)}\,d\sigma_n(v)\,d\sigma_n(u).

The numerator is the absolute bilinear form of the difference $X-Y$ , exactly as in the Problem 1 integrand, but the two quadratic forms in the denominator are taken from independent matrices: $P$ is paired with the outer variable $u$ and $Q$ with the inner variable $v$ . Setting $P=X$ and $Q=Y$ recovers the Problem 1 distance $d(X,Y)$ .

This object is the natural interpolation device when the diagonal denominator pair $(X,Y)$ is replaced by a larger pair such as $(A+B,\,C+D)$ : it separates numerator effects (the difference being integrated) from denominator effects (the regularising quadratic forms), and it is what makes the additive Problem 1 inequality decompose into a numerator-subadditivity step and a denominator-normalisation step.

Formalization Note Real division is total: at a pair $(u,v)$ where a denominator factor is $0$ the integrand is $0$ , and a non-integrable inner or outer integrand makes the corresponding Bochner integral $0$ . For $n=0$ the sphere is empty and the value is $0$ . The definition reuses bilinear and surfaceMeasure from the Problem 1 definition module Def_rybin2026_p01_matrix_integral.

Definition code

import Definitions.Def_rybin2026_p01_matrix_integral

open Matrix MeasureTheory Metric
open scoped BigOperators

namespace RybinAI2026.P01

/-- Mixed spherical double integral.  The numerator measures the bilinear form of the
difference `X - Y` on the pair of unit vectors, while the two quadratic forms in the
denominator are taken from *independent* matrices `P` (paired with `u`) and `Q` (paired
with `v`).  Taking `P = X` and `Q = Y` recovers `distance X Y`.  Real division is total:
where a denominator factor vanishes the integrand at that pair is `0`, and a non-integrable
integrand contributes `0`. -/
noncomputable def crossIntegral {n : ℕ}
    (X Y P Q : Matrix (Fin n) (Fin n) ℝ) : ℝ :=
  ∫ u, ∫ v,
    |bilinear (X - Y) u.1 v.1| /
      (bilinear P u.1 u.1 * bilinear Q v.1 v.1)
    ∂surfaceMeasure n ∂surfaceMeasure n

/-- `distance` is the diagonal case `P = X`, `Q = Y` of `crossIntegral`. -/
theorem distance_eq_crossIntegral {n : ℕ} (X Y : Matrix (Fin n) (Fin n) ℝ) :
    distance X Y = crossIntegral X Y X Y := rfl

end RybinAI2026.P01

Source

https://rybindmitry.github.io/problems/1.html , CUHK-Shenzhen AI Math Problems, Problem 1 (Positive definite matrix integral inequality). Auxiliary object for decomposing the additive inequality: generalises the displayed spherical-integral distance d(X,Y) by decoupling the two denominator matrices.

View graph

Mixed spherical integral crossIntegral⁡(X,Y,P,Q)\operatorname{crossIntegral}(X,Y,P,Q)crossIntegral(X,Y,P,Q)

Mixed spherical integral $\operatorname{crossIntegral}(X,Y,P,Q)$