Log-convexity of the mixed integral along a denominator ray

Proved

RybinAI2026.P01.crossIntegral_add_logConvex

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

integral-inequalitylog-convexitymatrix-analysispositive-definite-matrices

Let $X,Y,A,B,C$ be real square matrices of the same size, and assume that $A,B,C$ are symmetric positive definite. For a numerator $X-Y$ , write $K_{P,Q}(X-Y)$ for the mission's mixed double spherical integral with positive-definite quadratic denominators $P$ and $Q$ . Then

K_{A+B,C}(X-Y)^2\leq K_{A,C}(X-Y)\,K_{A+2B,C}(X-Y),

and, symmetrically in the second sphere variable,

K_{C,A+B}(X-Y)^2\leq K_{C,A}(X-Y)\,K_{C,A+2B}(X-Y).

Thus the mixed integral is midpoint log-convex when either positive quadratic denominator moves along the ray $A+tB$ . This supplies a reusable square-contraction step for reductions of the matrix-integral addition problem.

Formalization Note The Lean expression ((A+B)+B) represents $A+2B$ . The theorem retains the original unnormalized spherical surface measure and also covers the zero-dimensional case.

Preamble

import Definitions.Def_rybin2026_p01_cross_integral

set_option autoImplicit false

open Matrix RybinAI2026.P01

Formal statement

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

Source

Derived denominator log-convexity lemma for CUHK-Shenzhen AI Math Problems, Problem 1 (Prof. Cosme Louart), https://rybindmitry.github.io/problems/1.html; the source supplies the mixed spherical kernel, while this reusable consequence is proved directly from that definition.

View graph