Subadditivity of the matrix integral distance: $d(A+B,C+D)\le d(A,C)+d(B,D)$

Proved

RybinAI2026.P01.distance_add_le_add

by evgeth · Sep 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

integral-inequalitymatrix-analysispositive-definite-matrices

Let $n\ge 0$ and let $A,B,C,D$ be real symmetric positive definite $n\times n$ matrices, and let $d$ be the distance of CUHK-Shenzhen AI Math Problem 1,

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

Then

d(A+B,\,C+D)\;\le\; d(A,C)+d(B,D).

This is the additive (weak) form of the mission target RybinAI2026.P01.matrix_integral_inequality, which asserts the same bound with $\max(d(A,C),d(B,D))$ in place of the sum. The gap between the two is exactly the open content of Problem 1: the pointwise identity behind subadditivity splits the integrand of $d(A+B,C+D)$ into the two kernels with weights $a(u)c(v)$ and $(1-a(u))(1-c(v))$ , $a=u^{\mathsf T}Au/u^{\mathsf T}(A+B)u$ , $c=v^{\mathsf T}Cv/v^{\mathsf T}(C+D)v$ , whose sum is at most one pointwise but is averaged against two different measures.

Formalization note. distance, bilinear and surfaceMeasure are the mission's definitions; Matrix.PosDef includes symmetry. No hypothesis 0 < n is needed.

Preamble

import Definitions.Def_rybin2026_p01_matrix_integral

open Matrix MeasureTheory

Formal statement

namespace RybinAI2026.P01

/-- Subadditivity. -/
theorem distance_add_le_add {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) ≤ distance A C + distance B D := by
  sorry

end RybinAI2026.P01

Source

Unconditional structural property / special case of CUHK-Shenzhen AI Math Problem 1 (Prof. Cosme Louart), https://rybindmitry.github.io/problems/1.html; Prove2Me mission 'Positive definite matrix integral inequality' (c36fd4df); no literature source.

View graph

Subadditivity of the matrix integral distance: d(A+B,C+D)≤d(A,C)+d(B,D)d(A+B,C+D)\le d(A,C)+d(B,D)d(A+B,C+D)≤d(A,C)+d(B,D)

Subadditivity of the matrix integral distance: $d(A+B,C+D)\le d(A,C)+d(B,D)$