Exact variance slack for cross-integral denominator addition

Proved

RybinAI2026.P01.crossIntegral_add_harmonic_slack

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

integral-inequalitymatrix-analysisvariance

Fix arbitrary numerator matrices $X,Y$ and positive-definite denominator matrices $A,B,C$ . Write

I=\operatorname{crossIntegral}(X,Y,A,C),\quad J=\operatorname{crossIntegral}(X,Y,B,C),\quad H=\operatorname{crossIntegral}(X,Y,A+B,C).

Let $h(u,v)$ be the $H$ -integrand and let $r(u,v)=(u^{\mathsf T}Bu)/(u^{\mathsf T}Au)$ . With $\mu$ the product of the original sphere surface measures, define

V=\iint h(z)h(w)\frac{(r(z)-r(w))^2}{r(z)r(w)}\,d\mu(z)\,d\mu(w).

Then the harmonic denominator inequality has the exact slack

IJ-H(I+J)=\frac12V.

Thus its loss is precisely a nonnegative weighted variance of the quadratic-form ratio. The formula remains valid in dimension zero and uses the original unnormalized measure. It is intended for retaining the variation discarded by the parallel-sum estimate in Problem 1.

Preamble

import Definitions.Def_rybin2026_p01_cross_integral
import Theorems.Thm_RybinAI2026_P01_harmonic_variance_identity

open Matrix MeasureTheory Metric RybinAI2026.P01

Formal statement

theorem RybinAI2026.P01.crossIntegral_add_harmonic_slack {n : ℕ}
    (X Y A B C : Matrix (Fin n) (Fin n) ℝ)
    (hA : A.PosDef) (hB : B.PosDef) (hC : C.PosDef) :
    let S := sphere (0 : Euclidean n) 1
    let μ := (surfaceMeasure n).prod (surfaceMeasure n)
    let h (z : S × S) :=
      |bilinear (X-Y) z.1.1 z.2.1| /
        (bilinear (A+B) z.1.1 z.1.1 * bilinear C z.2.1 z.2.1)
    let r (z : S × S) := bilinear B z.1.1 z.1.1 / bilinear A z.1.1 z.1.1
    let V := ∫ z : (S × S) × (S × S),
      h z.1*h z.2*(r z.1-r z.2)^2/(r z.1*r z.2) ∂(μ.prod μ)
    crossIntegral X Y A C * crossIntegral X Y B C -
        crossIntegral X Y (A+B) C *
          (crossIntegral X Y A C + crossIntegral X Y B C) =
      (1/2 : ℝ)*V := by
  sorry

Source

https://rybindmitry.github.io/problems/1.html, Problem 1 and its mixed denominator integrals. Derived specialization of the proved harmonic variance identity; the source states the general problem, not this exact slack formula.

View graph