Harmonic contraction under addition of a quadratic denominator

Proved

RybinAI2026.P01.crossIntegral_add_harmonic

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

integral-inequalitymatrix-analysispositive-definite-matrices

Let $X,Y$ be arbitrary real $n\times n$ matrices and let $A,B,C,D$ be real symmetric positive-definite matrices. Write $K(P,Q)=\operatorname{crossIntegral}(X,Y,P,Q)$ for the mixed spherical integral whose fixed numerator is $|u^{\mathsf T}(X-Y)v|$ and whose denominator is $(u^{\mathsf T}Pu)(v^{\mathsf T}Qv)$ . Then addition in either denominator satisfies the cleared harmonic-mean bounds

K(A+B,C)\bigl(K(A,C)+K(B,C)\bigr)\le K(A,C)K(B,C),

and

K(A,C+D)\bigl(K(A,C)+K(A,D)\bigr)\le K(A,C)K(A,D).

When the two integrals on the right are positive, these say that the integral after denominator addition is bounded by their parallel sum $(I^{-1}+J^{-1})^{-1}$ . The cleared form also covers a zero numerator and the empty zero-dimensional sphere without division. This estimate is useful for controlling the denominator-normalization step in Problem 1.

Preamble

import Definitions.Def_rybin2026_p01_cross_integral

open Matrix RybinAI2026.P01

Formal statement

theorem RybinAI2026.P01.crossIntegral_add_harmonic {n : ℕ}
    (X Y A B C D : Matrix (Fin n) (Fin n) ℝ)
    (hA : A.PosDef) (hB : B.PosDef) (hC : C.PosDef) (hD : D.PosDef) :
    (crossIntegral X Y (A+B) C *
        (crossIntegral X Y A C + crossIntegral X Y B C) ≤
      crossIntegral X Y A C * crossIntegral X Y B C) ∧
    (crossIntegral X Y A (C+D) *
        (crossIntegral X Y A C + crossIntegral X Y A D) ≤
      crossIntegral X Y A C * crossIntegral X Y A D) := by
  sorry

Source

https://rybindmitry.github.io/problems/1.html, Problem 1 and its defining integral. Derived auxiliary denominator-contraction estimate; the source states the general matrix-integral problem, not this separate lemma.

View graph