Square-summable coefficients for adding one quadratic denominator

Open

RybinAI2026.P01.crossIntegral_add_l2_coefficients

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

integral-inequalitymatrix-analysispositive-definite-matrices

Let $A$ and $B$ be real symmetric positive-definite $n\times n$ matrices. There should exist nonnegative constants $\alpha$ and $\beta$ , depending only on $A$ and $B$ , such that

\alpha^2+\beta^2\leq1.

Adding $B$ to the first quadratic denominator contracts every mixed spherical integral by $\alpha$ relative to denominator $A$ and by $\beta$ relative to denominator $B$ . The same two constants work when the addition is made in the second sphere variable. Explicitly, for every numerator $X-Y$ and every positive-definite other denominator $P$ ,

K_{A+B,P}(X-Y)\leq\alpha K_{A,P}(X-Y),\qquad K_{A+B,P}(X-Y)\leq\beta K_{B,P}(X-Y).

The analogous two inequalities hold for $K_{P,A+B}$ . Here $K$ is the mission's crossIntegral with the original unnormalized surface measure.

This one-sphere coefficient statement is a sufficient analytic core for CUHK-Shenzhen AI Math Problem 1. Applying it to $(A,B)$ and $(C,D)$ makes the two coefficients multiply across the sphere variables; Cauchy--Schwarz then makes their products sum to at most one.

Preamble

import Definitions.Def_rybin2026_p01_cross_integral

open Matrix RybinAI2026.P01

Formal statement

theorem RybinAI2026.P01.crossIntegral_add_l2_coefficients
    {n : ℕ} (A B : Matrix (Fin n) (Fin n) ℝ)
    (hA : A.PosDef) (hB : B.PosDef) :
    ∃ α β : ℝ,
      0 ≤ α ∧ 0 ≤ β ∧ α ^ 2 + β ^ 2 ≤ 1 ∧
      ∀ (X Y P : Matrix (Fin n) (Fin n) ℝ), P.PosDef →
        (crossIntegral X Y (A + B) P ≤ α * crossIntegral X Y A P) ∧
        (crossIntegral X Y (A + B) P ≤ β * crossIntegral X Y B P) ∧
        (crossIntegral X Y P (A + B) ≤ α * crossIntegral X Y P A) ∧
        (crossIntegral X Y P (A + B) ≤ β * crossIntegral X Y P B) := by
  sorry

Source

Derived sufficient lemma for CUHK-Shenzhen AI Math Problems, Problem 1, https://rybindmitry.github.io/problems/1.html; no external literature source is claimed.

View graph