Symmetry of the matrix integral distance: $d(A,B)=d(B,A)$

Proved

RybinAI2026.P01.distance_comm

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

integral-inequalitymatrix-analysispositive-definite-matrices

Let $n\ge 0$ and let $A,B$ be real symmetric positive definite $n\times n$ matrices. With $d$ 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),

one has $d(A,B)=d(B,A)$ . Although the integrand pairs the first matrix with $u$ and the second with $v$ , the distance is symmetric, because the bilinear form of the symmetric matrix $A-B$ is symmetric in $(u,v)$ and the two sphere variables can be exchanged. Symmetry allows both orderings of a pair to be used in the mission target RybinAI2026.P01.matrix_integral_inequality.

Formalization note. distance, bilinear and surfaceMeasure are the mission's definitions; Matrix.PosDef supplies the symmetry of $A$ and $B$ and the integrability of the integrand.

Preamble

import Definitions.Def_rybin2026_p01_matrix_integral

open Matrix MeasureTheory

Formal statement

namespace RybinAI2026.P01

/-- Symmetry. -/
theorem distance_comm {n : ℕ} (A B : Matrix (Fin n) (Fin n) ℝ) (hA : A.PosDef) (hB : B.PosDef) :
    distance A B = distance B A := 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

Symmetry of the matrix integral distance: d(A,B)=d(B,A)d(A,B)=d(B,A)d(A,B)=d(B,A)

Symmetry of the matrix integral distance: $d(A,B)=d(B,A)$