Directional doubled-denominator budget $\sup R_1+\sup R_2\le1$

Disproved

RybinAI2026.P01.sphere_direction_double_budget

by Steve1136 · Sep 21, 2026 · Mathlib c5ea003 (Lean v4.30.0)

integral-inequalitymatrix-analysispositive-definite-matrices

Let $A,B$ be real symmetric positive-definite $n\times n$ matrices, write $a(u)=u^{\mathsf T}Au$ and $b(u)=u^{\mathsf T}Bu$ , and let $\sigma$ be the mission's unnormalised surface measure on the unit sphere $S\subset\mathbb R^n$ . Then there are constants $p,q\ge0$ with $p+q\le1$ , depending only on $A$ and $B$ , such that for every direction $w\in\mathbb R^n$

\int_S\frac{|\langle u,w\rangle|}{a+2b}\,d\sigma\le p\int_S\frac{|\langle u,w\rangle|}{a}\,d\sigma,\qquad \int_S\frac{|\langle u,w\rangle|}{2a+b}\,d\sigma\le q\int_S\frac{|\langle u,w\rangle|}{b}\,d\sigma.

Equivalently, with $R_1(w)$ and $R_2(w)$ the two ratios (for $w\ne0$ ),

\sup_{w}R_1(w)+\sup_{w}R_2(w)\le1.

This is the one-sphere, rank-one core of crossIntegral_add_double_l1_coefficients, and in fact equivalent to it: rank-one numerators $M=w\,e_1^{\mathsf T}$ recover exactly these ratios.

In dimension one it is the scalar inequality $\frac{1}{1+2t}+\frac{t}{2+t}\le1$ for $t=b/a>0$ . If the generalised eigenvalues of $B$ relative to $A$ lie in $[m,M]$ with $M\le4m$ , it follows from the pointwise bounds $R_1\le\frac1{1+2m}$ and $R_2\le\frac{M}{2+M}$ . In general a pointwise argument cannot work: the weights $|\langle u,w\rangle|/a$ and $|\langle u,w\rangle|/b$ must be used.

Status. Open. A numerical search in $n=2,3$ (quadrature plus Nelder–Mead over $A,B$ ) found no violation; the value $1$ is approached only in degenerate limits where one matrix dominates the other. Lean writes $A+2B$ as ((A+B)+B), $2A+B$ as ((A+B)+A), and $\langle u,w\rangle$ as bilinear 1 u w.

Preamble

import Definitions.Def_rybin2026_p01_cross_integral

set_option autoImplicit false

open Matrix MeasureTheory RybinAI2026.P01

Formal statement

theorem RybinAI2026.P01.sphere_direction_double_budget
    {n : ℕ} (A B : Matrix (Fin n) (Fin n) ℝ)
    (hA : A.PosDef) (hB : B.PosDef) :
    ∃ p q : ℝ, 0 ≤ p ∧ 0 ≤ q ∧ p + q ≤ 1 ∧
      ∀ w : Euclidean n,
        (∫ u, |bilinear (1 : Matrix (Fin n) (Fin n) ℝ) u.1 w| / bilinear ((A+B)+B) u.1 u.1
            ∂surfaceMeasure n ≤
          p * ∫ u, |bilinear (1 : Matrix (Fin n) (Fin n) ℝ) u.1 w| / bilinear A u.1 u.1
            ∂surfaceMeasure n) ∧
        (∫ u, |bilinear (1 : Matrix (Fin n) (Fin n) ℝ) u.1 w| / bilinear ((A+B)+A) u.1 u.1
            ∂surfaceMeasure n ≤
          q * ∫ u, |bilinear (1 : Matrix (Fin n) (Fin n) ℝ) u.1 w| / bilinear B u.1 u.1
            ∂surfaceMeasure n) := by
  sorry

Source

Reformulation of Prove2Me theorem RybinAI2026.P01.crossIntegral_add_double_l1_coefficients (mission: Positive definite matrix integral inequality; original problem https://rybindmitry.github.io/problems/1.html)

View graph

Directional doubled-denominator budget sup⁡R1+sup⁡R2≤1\sup R_1+\sup R_2\le1supR1​+supR2​≤1

Directional doubled-denominator budget $\sup R_1+\sup R_2\le1$