Prove2Me

Common translation contracts the matrix integral distance: d(A+E,C+E)≤d(A,C)d(A+E,C+E)\le d(A,C)

Proved
RybinAI2026.P01.distance_add_right_le

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

integral-inequalitymatrix-analysispositive-definite-matrices

Let n≥0n\ge 0 and let A,C,EA,C,E be real symmetric positive definite n×nn\times n matrices. Let dd be the distance of CUHK-Shenzhen AI Math Problem 1,

d(X,Y)=∬Sn−1×Sn−1∣uT(X−Y)v∣(uTXu) (vTYv) dσ(u) dσ(v),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),

with σ\sigma the (unnormalised) surface measure toSphere of Lebesgue measure. Then

d(A+E, C+E)  ≤  d(A,C).d(A+E,\,C+E)\;\le\; d(A,C).

Adding the same positive definite matrix to both arguments can only decrease the distance. This is the case B=D=EB=D=E of the mission target RybinAI2026.P01.matrix_integral_inequality: there the right-hand side is max⁡(d(A,C),d(E,E))=d(A,C)\max(d(A,C),d(E,E))=d(A,C). It is the first of a family of unconditional structural properties of dd (translation monotonicity, subadditivity, symmetry, homogeneity) that any proof of the full conjecture can build on.

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

/-- Common translation contracts the distance. -/
theorem distance_add_right_le {n : ℕ} (A C E : Matrix (Fin n) (Fin n) ℝ)
    (hA : A.PosDef) (hC : C.PosDef) (hE : E.PosDef) :
    distance (A + E) (C + E) ≤ distance A C := 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