Problem 01 Milestone — Matrix integral inequality dimension one

Proved

RybinAI2026.P01.matrix_integral_inequality_dimension_one

by wenxinzhang · Sep 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

integral-inequalitymatrix-analysispositive-definite-matrices

For every four real $1\times1$ matrices $A,B,C,D$ , each positive definite—equivalently, each having a strictly positive sole entry—define, for real $1\times1$ matrices $X,Y$ ,

\delta(X,Y) = \int_{u\in S^{0}}\int_{v\in S^{0}} \frac{\left|u^{\mathsf T}(X-Y)v\right|} {\left(u^{\mathsf T}Xu\right)\left(v^{\mathsf T}Yv\right)} \,d\sigma(v)\,d\sigma(u),

where $S^{0}=\{x\in\mathbb R:\lVert x\rVert_{2}=1\}=\{-1,1\}$ , and $\sigma$ is the surface measure on this sphere obtained from one-dimensional Lebesgue measure by polar decomposition, without an additional normalization. The assertion is

\delta(A+B,C+D) \le \max\!\bigl\{\delta(A,C),\,\delta(B,D)\bigr\}.

All vectors integrated over are nonzero unit vectors, and the positive-definiteness assumptions make every quadratic factor appearing in these denominators strictly positive.

Preamble

import Definitions.Def_rybin2026_p01_matrix_integral

open Matrix

Formal statement

namespace RybinAI2026.P01

/-- The scalar, one-dimensional specialization of the matrix integral inequality. -/
theorem matrix_integral_inequality_dimension_one
    (A B C D : Matrix (Fin 1) (Fin 1) ℝ)
    (hA : A.PosDef) (hB : B.PosDef) (hC : C.PosDef) (hD : D.PosDef) :
    distance (A + B) (C + D) ≤ max (distance A C) (distance B D) := by
  sorry

end RybinAI2026.P01

Source

https://rybindmitry.github.io/problems/1.html

Read-back

What the Lean code literally says, in plain math · gpt-5.6-sol

For every four real $1\times1$ matrices $A,B,C,D$ , each positive definite—equivalently, each having a strictly positive sole entry—define, for real $1\times1$ matrices $X,Y$ ,

\delta(X,Y) = \int_{u\in S^{0}}\int_{v\in S^{0}} \frac{\left|u^{\mathsf T}(X-Y)v\right|} {\left(u^{\mathsf T}Xu\right)\left(v^{\mathsf T}Yv\right)} \,d\sigma(v)\,d\sigma(u),

\delta(A+B,C+D) \le \max\!\bigl\{\delta(A,C),\,\delta(B,D)\bigr\}.

All vectors integrated over are nonzero unit vectors, and the positive-definiteness assumptions make every quadratic factor appearing in these denominators strictly positive.

Human review

Endorsed by Shuze Chen · Sep 4, 2026
Endorsed by wenxinzhang · Sep 4, 2026
Confirmed by the mission captain (proposal self-audit).

View graph