Square-root denominator reduction for the matrix-integral inequality

Proved

RybinAI2026.P01.matrix_integral_sqrt_denominator_reduction

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

integral-inequalitymatrix-analysispositive-definite-matrices

Let $A,B,C,D$ be real symmetric positive-definite $n\times n$ matrices. For unit vectors $u,v$ , write

a=u^{\mathsf T}Au,\quad b=u^{\mathsf T}Bu,\quad c=v^{\mathsf T}Cv,\quad d=v^{\mathsf T}Dv,

and let $x=u^{\mathsf T}(A-C)v$ , $y=u^{\mathsf T}(B-D)v$ . Then the Problem 1 distance after addition is bounded by

d(A+B,C+D)\le\iint\frac{|x|+|y|}{(\sqrt{ac}+\sqrt{bd})^2}\,d\sigma(u)\,d\sigma(v),

where $\sigma$ is the original unnormalized sphere surface measure. This gives a structured global intermediate for Problem 1: proving that the displayed integral is at most $\max\{d(A,C),d(B,D)\}$ would settle the target. The statement also includes dimension zero.

Preamble

import Definitions.Def_rybin2026_p01_matrix_integral

open Matrix MeasureTheory Metric RybinAI2026.P01

Formal statement

theorem RybinAI2026.P01.matrix_integral_sqrt_denominator_reduction {n : ℕ}
    (A B C D : Matrix (Fin n) (Fin n) ℝ)
    (hA : A.PosDef) (hB : B.PosDef) (hC : C.PosDef) (hD : D.PosDef) :
    distance (A+B) (C+D) ≤
      ∫ z : sphere (0 : Euclidean n) 1 × sphere (0 : Euclidean n) 1,
        (|bilinear (A-C) z.1.1 z.2.1|+|bilinear (B-D) z.1.1 z.2.1|) /
          (√(bilinear A z.1.1 z.1.1*bilinear C z.2.1 z.2.1)+
            √(bilinear B z.1.1 z.1.1*bilinear D z.2.1 z.2.1))^2
        ∂((surfaceMeasure n).prod (surfaceMeasure n)) := by
  sorry

Source

CUHK-Shenzhen AI Math Problems, Problem 1, https://rybindmitry.github.io/problems/1.html. The square-root denominator is motivated by the scalar addition estimate in Louart--Couillet, A Concentration of Measure and Random Matrix Approach to Large Dimensional Robust Statistics, arXiv:2006.09728, Property 3.6 and Lemma 3.7.

View graph