Directional bounds on a denominator change lift to crossIntegral

Proved

RybinAI2026.P01.crossIntegral_le_of_rankOne_le

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

integral-inequalitymatrix-analysispositive-definite-matrices

Let $A$ and $D$ be real symmetric positive-definite $n\times n$ matrices, let $\sigma$ be the mission's unnormalised surface measure on the unit sphere $S\subset\mathbb R^n$ , and let $\rho\in\mathbb R$ . Suppose that for every vector $w\in\mathbb R^n$

\int_S\frac{|\langle u,w\rangle|}{u^{\mathsf T}Du}\,d\sigma(u)\;\le\;\rho\int_S\frac{|\langle u,w\rangle|}{u^{\mathsf T}Au}\,d\sigma(u).

Then for all real matrices $X,Y$ and every positive-definite $P$ , the mixed spherical integral $K$ (crossIntegral) satisfies

K(X,Y,D,P)\le\rho\,K(X,Y,A,P)\qquad\text{and}\qquad K(X,Y,P,D)\le\rho\,K(X,Y,P,A).

Why it is true. Put $M=X-Y$ . In the first slot, Fubini gives

K(X,Y,D,P)=\int_S\frac{1}{v^{\mathsf T}Pv}\int_S\frac{|\langle u,Mv\rangle|}{u^{\mathsf T}Du}\,d\sigma(u)\,d\sigma(v).

Applying the hypothesis with $w=Mv$ bounds the inner integral, and the weight $1/(v^{\mathsf T}Pv)$ is positive. In the second slot, $|u^{\mathsf T}Mv|=|\langle v,M^{\mathsf T}u\rangle|$ , so apply the hypothesis to the inner $v$ -integral with $w=M^{\mathsf T}u$ . All integrands are continuous on the compact sphere (or its square) because the denominators are strictly positive there, so every integral is finite and Fubini applies. In dimension $0$ the sphere is empty and all integrals vanish.

This is the infrastructure step saying that a directional (rank-one numerator) bound on a denominator change lifts to the full mixed double integral in either slot. Lean writes $\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.crossIntegral_le_of_rankOne_le
    {n : ℕ} (A D : Matrix (Fin n) (Fin n) ℝ)
    (hA : A.PosDef) (hD : D.PosDef) (ρ : ℝ)
    (h : ∀ w : Euclidean n,
      ∫ u, |bilinear (1 : Matrix (Fin n) (Fin n) ℝ) u.1 w| / bilinear D u.1 u.1
          ∂surfaceMeasure n ≤
        ρ * ∫ u, |bilinear (1 : Matrix (Fin n) (Fin n) ℝ) u.1 w| / bilinear A u.1 u.1
          ∂surfaceMeasure n) :
    ∀ (X Y P : Matrix (Fin n) (Fin n) ℝ), P.PosDef →
      crossIntegral X Y D P ≤ ρ * crossIntegral X Y A P ∧
      crossIntegral X Y P D ≤ ρ * crossIntegral X Y P A := 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