Doubled-denominator coefficient budget for two numerators

Disproved

RybinAI2026.P01.crossIntegral_add_double_pair_coefficients

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

integral-inequalitymatrix-analysispositive-definite-matriceszonoids

Let $A$ and $B$ be real symmetric positive-definite matrices. Fix two matrix numerators $M_1=X-Y$ and $M_2=U-V$ , together with two positive-definite other denominators $P$ and $Q$ . Then there should exist nonnegative coefficients $p,q$ with $p+q\leq1$ such that

K_{A+2B,P}(M_1)\leq pK_{A,P}(M_1),\qquad K_{2A+B,Q}(M_2)\leq qK_{B,Q}(M_2).

There should also exist, independently, nonnegative $r,s$ with $r+s\leq1$ for the corresponding second-variable estimates

K_{P,A+2B}(M_1)\leq rK_{P,A}(M_1),\qquad K_{Q,2A+B}(M_2)\leq sK_{Q,B}(M_2).

Here $K$ is the mission's mixed double spherical integral with unnormalized surface measure. The coefficients may depend on the two specified numerators and other denominators; no uniformity over all possible numerators is asserted.

This pairwise form is sufficient for the original four-matrix problem. Midpoint log-convexity converts each linear doubled-denominator contraction into a square-root contraction at $A+B$ , while the two coefficient pairs combine by the ordinary two-dimensional Cauchy–Schwarz inequality.

Formalization Note Lean writes $A+2B$ as ((A+B)+B) and $2A+B$ as ((A+B)+A). Left-slot and right-slot coefficient pairs are allowed to differ.

Preamble

import Definitions.Def_rybin2026_p01_cross_integral

set_option autoImplicit false

open Matrix RybinAI2026.P01

Formal statement

theorem RybinAI2026.P01.crossIntegral_add_double_pair_coefficients
    {n : ℕ} (A B : Matrix (Fin n) (Fin n) ℝ)
    (hA : A.PosDef) (hB : B.PosDef) :
    ∀ (X Y U V P Q : Matrix (Fin n) (Fin n) ℝ), P.PosDef → Q.PosDef →
      (∃ p q : ℝ, 0 ≤ p ∧ 0 ≤ q ∧ p+q ≤ 1 ∧
        crossIntegral X Y ((A+B)+B) P ≤ p*crossIntegral X Y A P ∧
        crossIntegral U V ((A+B)+A) Q ≤ q*crossIntegral U V B Q) ∧
      (∃ r s : ℝ, 0 ≤ r ∧ 0 ≤ s ∧ r+s ≤ 1 ∧
        crossIntegral X Y P ((A+B)+B) ≤ r*crossIntegral X Y P A ∧
        crossIntegral U V Q ((A+B)+A) ≤ s*crossIntegral U V Q B) := by
  sorry

Source

Derived pairwise coefficient frontier for CUHK-Shenzhen AI Math Problems, Problem 1 (Prof. Cosme Louart), https://rybindmitry.github.io/problems/1.html; based on the proved Prove2Me midpoint log-convexity theorem RybinAI2026.P01.crossIntegral_add_logConvex (02cf0844-154e-494e-ad1e-1c75cffc0605).

View graph