Matrix-integral bound from a convex mixture of row isometries

Proved

RybinAI2026.P01.matrix_integral_inequality_row_isometry_mix

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

integral-inequalitymatrix-analysispositive-definite-matrices

Let $n$ be a natural number and let $A,B,C,D$ be real symmetric positive-definite $n\times n$ matrices. Write $\beta_M(u,v)=u^{\mathsf T}Mv$ and let $d$ be the original unnormalized double spherical integral. Let $T$ be a real linear isometric equivalence of Euclidean space and let $t\in[0,1]$ . Suppose $T$ preserves the quadratic form of $B$ :

\beta_B(Tu,Tu)=\beta_B(u,u)\qquad\text{for every }u.

Suppose also that the output numerator is the following convex mixture:

\beta_{(A+B)-(C+D)}(u,v) =t\,\beta_{B-D}(u,v)+(1-t)\,\beta_{B-D}(Tu,v) \qquad\text{for every }u,v.

Then

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

This is a sufficient condition for the maximum inequality in Problem 1, including equality endpoints t=0 and t=1. It uses a symmetry of the denominator quadratic form to compare integrated numerators, and need not give a pointwise bound by the original input kernel. It imposes neither a commutativity assumption on all four matrices nor an arbitrary congruence invariance rule. Dimension zero is allowed by the formal statement.

Preamble

import Definitions.Def_rybin2026_p01_matrix_integral

open Matrix RybinAI2026.P01

Formal statement

theorem RybinAI2026.P01.matrix_integral_inequality_row_isometry_mix {n : ℕ}
    (A B C D : Matrix (Fin n) (Fin n) ℝ)
    (hA : A.PosDef) (hB : B.PosDef) (hC : C.PosDef) (hD : D.PosDef)
    (e : Euclidean n ≃ₗᵢ[ℝ] Euclidean n) (t : ℝ) (ht : 0 ≤ t) (ht1 : t ≤ 1)
    (hBsym : ∀ u : Euclidean n, bilinear B (e u) (e u) = bilinear B u u)
    (hnum : ∀ u v : Euclidean n,
      bilinear ((A+B)-(C+D)) u v =
        t * bilinear (B-D) u v + (1-t) * bilinear (B-D) (e u) v) :
    distance (A+B) (C+D) ≤ distance B D := by
  sorry

Source

https://rybindmitry.github.io/problems/1.html, Problem 1 and its defining integral. Derived sufficient condition using convexity of absolute value and denominator-preserving orthogonal changes of variables; not a separately stated theorem in the source.

View graph