Four-way harmonic bound for both added quadratic denominators

Proved

RybinAI2026.P01.crossIntegral_add_four_harmonic

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

integral-inequalitymatrix-analysispositive-definite-matrices

Fix arbitrary real $n\times n$ numerator matrices $X,Y$ and real symmetric positive-definite denominator matrices $A,B,C,D$ . Define

a=K(A,C),\quad b=K(A,D),\quad c=K(B,C),\quad d=K(B,D),\quad k=K(A+B,C+D),

where $K(P,Q)=\operatorname{crossIntegral}(X,Y,P,Q)$ keeps the numerator $|u^{\mathsf T}(X-Y)v|$ fixed. Then

k\,(bcd+acd+abd+abc)\le abcd.

When $a,b,c,d$ are positive, this is the four-way parallel-sum estimate

k\le\left(\frac1a+\frac1b+\frac1c+\frac1d\right)^{-1}.

The cleared form also covers a zero numerator and the empty zero-dimensional sphere. This estimate bounds the full product denominator after both additions and can be applied separately to the two numerator differences in Problem 1.

Preamble

import Definitions.Def_rybin2026_p01_cross_integral

open Matrix RybinAI2026.P01

Formal statement

theorem RybinAI2026.P01.crossIntegral_add_four_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) :
    let a := crossIntegral X Y A C
    let b := crossIntegral X Y A D
    let c := crossIntegral X Y B C
    let d := crossIntegral X Y B D
    let k := crossIntegral X Y (A+B) (C+D)
    k*(b*c*d+a*c*d+a*b*d+a*b*c) ≤ a*b*c*d := by
  sorry

Source

https://rybindmitry.github.io/problems/1.html, Problem 1 and its defining integral. Derived consequence of the proved one-sided harmonic denominator contractions; the source states the general matrix-integral problem, not this separate lemma.

View graph