Moment upper and lower bounds for the spherical matrix integral

Proved

RybinAI2026.P01.distance_moment_bounds

by miao · Sep 8, 2026 · Mathlib c5ea003 (Lean v4.30.0)

integral-inequalitymatrix-analysispositive-definite-matrices

Let $X,Y$ be real symmetric positive-definite $n\times n$ matrices, with $n$ any natural number. Use the original surface measure $\sigma_n$ on the unit sphere, and write $d(X,Y)$ for the defining double spherical integral. For unit vectors $u,v$ , put

z(u,v)=u^{\mathsf T}(X-Y)v,\qquad H(u,v)=(u^{\mathsf T}Xu)(v^{\mathsf T}Yv).

Define the two moments with respect to the product of the original surface measures:

Q=\iint\frac{z(u,v)^2}{H(u,v)}\,d\sigma_n(u)\,d\sigma_n(v),\qquad R=\iint\frac{1}{H(u,v)}\,d\sigma_n(u)\,d\sigma_n(v).

Let $L$ be a real constant such that $|z(u,v)|\le L$ for all unit vectors $u,v$ . Then

2t\,d(X,Y)\le Q+t^2R\quad\text{for every }t\in\mathbb R,\qquad d(X,Y)^2\le QR,\qquad Q\le L\,d(X,Y).

These moment estimates retain the quadratic denominator and give upper and lower bounds for the matrix integral. Positive choices of $t$ and $L$ allow division to produce explicit bounds. They can support sufficient conditions for the maximum inequality in Problem 1, but do not assert that inequality for arbitrary quadruples. The moments here use unnormalized surface measure.

Formalization Note The statement also allows dimension zero and does not divide by a moment, by $L$ , or by the sphere area.

Preamble

import Definitions.Def_rybin2026_p01_matrix_integral
import Mathlib.MeasureTheory.Integral.Prod

open Matrix MeasureTheory Metric RybinAI2026.P01

Formal statement

theorem RybinAI2026.P01.distance_moment_bounds {n : ℕ} (X Y : Matrix (Fin n) (Fin n) ℝ)
    (hX : X.PosDef) (hY : Y.PosDef) (L : ℝ)
    (hbound : ∀ u v : sphere (0 : Euclidean n) 1,
      |bilinear (X-Y) u.1 v.1| ≤ L) :
    let μ := (surfaceMeasure n).prod (surfaceMeasure n)
    let Q := ∫ p : sphere (0 : Euclidean n) 1 × sphere (0 : Euclidean n) 1,
      (bilinear (X-Y) p.1.1 p.2.1)^2 /
        (bilinear X p.1.1 p.1.1 * bilinear Y p.2.1 p.2.1) ∂μ
    let R := ∫ p : sphere (0 : Euclidean n) 1 × sphere (0 : Euclidean n) 1,
      1 / (bilinear X p.1.1 p.1.1 * bilinear Y p.2.1 p.2.1) ∂μ
    (∀ t : ℝ, 2*t*distance X Y ≤ Q+t^2*R) ∧
      (distance X Y)^2 ≤ Q*R ∧ Q ≤ L*distance X Y := by
  sorry

Source

https://rybindmitry.github.io/problems/1.html, Problem 1 and its defining integral. Derived auxiliary estimates from the nonnegativity of the weighted square (|u^T(X-Y)v|-t)^2/H and a uniform numerator bound; not a separately stated theorem in the source.

View graph