Matrix integral inequality for rational regularized Gram matrices

Open

RybinAI2026.P01.matrix_integral_inequality_rational_gram

by ryanshin · Sep 5, 2026 · Mathlib c5ea003 (Lean v4.30.0)

integral-inequalitymatrix-analysispositive-definite-matrices

Let $n>0$ and $k\geq 0$ be integers, and let $P,Q,R,S$ be rational $n\times n$ matrices. Regard their entries as real numbers, put $\varepsilon_k=1/(k+1)$ , and define

A=P^{\mathsf T}P+\varepsilon_k I_n,\qquad B=Q^{\mathsf T}Q+\varepsilon_k I_n,\qquad C=R^{\mathsf T}R+\varepsilon_k I_n,\qquad D=S^{\mathsf T}S+\varepsilon_k I_n.

For real positive-definite matrices $X,Y$ , write

d(X,Y)=\int_{S^{n-1}}\int_{S^{n-1}} \frac{|u^{\mathsf T}(X-Y)v|} {(u^{\mathsf T}Xu)(v^{\mathsf T}Yv)}\,d\sigma(v)\,d\sigma(u),

where $\sigma$ is the unnormalized surface measure obtained from Euclidean Lebesgue volume by polar decomposition. The assertion is

d(A+B,C+D)\leq\max\{d(A,C),d(B,D)\}.

Every matrix displayed above is positive definite, regardless of whether the rational matrices are singular. This is the restriction of Problem 1 to a countable family with rational entries and a common positive regularization parameter. It is the unresolved arithmetic case used by the approximation reduction of the general real-matrix problem; it is not asserted to have been proved.

Preamble

import Definitions.Def_rybin2026_p01_matrix_integral

open Matrix RybinAI2026.P01

Formal statement

theorem RybinAI2026.P01.matrix_integral_inequality_rational_gram
    {n : ℕ} (hn : 0 < n) (k : ℕ)
    (P Q R S : Matrix (Fin n) (Fin n) ℚ) :
    let p : Matrix (Fin n) (Fin n) ℝ := P.map (fun q : ℚ => (q : ℝ))
    let q : Matrix (Fin n) (Fin n) ℝ := Q.map (fun q : ℚ => (q : ℝ))
    let r : Matrix (Fin n) (Fin n) ℝ := R.map (fun q : ℚ => (q : ℝ))
    let s : Matrix (Fin n) (Fin n) ℝ := S.map (fun q : ℚ => (q : ℝ))
    let A := p.transpose * p + ((k : ℝ) + 1)⁻¹ • 1
    let B := q.transpose * q + ((k : ℝ) + 1)⁻¹ • 1
    let C := r.transpose * r + ((k : ℝ) + 1)⁻¹ • 1
    let D := s.transpose * s + ((k : ℝ) + 1)⁻¹ • 1
    distance (A + B) (C + D) ≤ max (distance A C) (distance B D) := by
  sorry

Source

https://rybindmitry.github.io/problems/1.html, Problem 1, restricted to rational Gram matrices with the common regularizer I/(k+1). The general statement is recovered by the separately formalized continuity and density reduction.

View graph