Prove2Me

Two-parameter diagonal matrix-integral inequality for a,d at least one

Proved
RybinAI2026.P01.matrix_integral_inequality_two_parameter_diagonal

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

integral-inequalitymatrix-analysispositive-definite-matrices

Let a,da,d be real numbers with a≥1a\geq1 and d≥1d\geq1, and set

A=diag⁡(1,a),B=diag⁡(a,1),C=I2,D=diag⁡(1,d).A=\operatorname{diag}(1,a),\qquad B=\operatorname{diag}(a,1),\qquad C=I_2,\qquad D=\operatorname{diag}(1,d).

Then, for the original unnormalized spherical matrix integral d2d_2 of Problem 1,

d2(A+B,C+D)≤max⁡{d2(A,C),d2(B,D)}.d_2(A+B,C+D)\leq\max\{d_2(A,C),d_2(B,D)\}.

All matrices are real symmetric and strictly positive definite, including the boundary values a=1 or d=1. This is a two-parameter restricted case of the matrix-integral conjecture. The input matrices are exactly as displayed; no independent rescaling or change of the defining measure is included. The scalar parameter d is distinct from the distance notation d_2.

Preamble
import Definitions.Def_rybin2026_p01_matrix_integral

open Matrix RybinAI2026.P01
Formal statement
theorem RybinAI2026.P01.matrix_integral_inequality_two_parameter_diagonal (a d : ℝ) (ha : 1 ≤ a) (hd : 1 ≤ d) :
    let A : Matrix (Fin 2) (Fin 2) ℝ := Matrix.diagonal ![1,a]
    let B : Matrix (Fin 2) (Fin 2) ℝ := Matrix.diagonal ![a,1]
    let C : Matrix (Fin 2) (Fin 2) ℝ := 1
    let D : Matrix (Fin 2) (Fin 2) ℝ := Matrix.diagonal ![1,d]
    distance (A+B) (C+D) ≤ max (distance A C) (distance B D) := by
  sorry
Source
https://rybindmitry.github.io/problems/1.html, Problem 1 specialized to A=diag(1,a), B=diag(a,1), C=I_2, D=diag(1,d), a,d>=1. Derived restricted case; not a separately stated source theorem.

View graph