Prove2Me

Doubled-denominator budget for one fixed numerator

Proved
RybinAI2026.P01.crossIntegral_double_add_same_numerator

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

integral-inequalitymatrix-analysispositive-definite-matrices

Fix a matrix numerator M=X−YM=X-Y and positive-definite quadratic denominators A,B,CA,B,C. Then the two doubled-denominator contractions satisfy the cleared normalized inequality

KA+2B,C(M)KB,C(M)+K2A+B,C(M)KA,C(M)≤KA,C(M)KB,C(M).K_{A+2B,C}(M)K_{B,C}(M)+K_{2A+B,C}(M)K_{A,C}(M)\leq K_{A,C}(M)K_{B,C}(M).

The analogous assertion holds when the doubled additions occur in the second sphere variable:

KC,A+2B(M)KC,B(M)+KC,2A+B(M)KC,A(M)≤KC,A(M)KC,B(M).K_{C,A+2B}(M)K_{C,B}(M)+K_{C,2A+B}(M)K_{C,A}(M)\leq K_{C,A}(M)K_{C,B}(M).

When the two input integrals are positive, the first inequality says

KA+2B,C(M)KA,C(M)+K2A+B,C(M)KB,C(M)≤1.\frac{K_{A+2B,C}(M)}{K_{A,C}(M)}+\frac{K_{2A+B,C}(M)}{K_{B,C}(M)}\leq1.

This is the fixed-numerator form of the linear doubled-denominator budget. It isolates uniformity over different numerators as the remaining issue in the corresponding coefficient theorem.

Formalization Note All formulas use the mission's original unnormalized surface measure. The cleared form includes vanishing numerators and dimension zero without division hypotheses.

Preamble
import Definitions.Def_rybin2026_p01_cross_integral

set_option autoImplicit false

open Matrix RybinAI2026.P01
Formal statement
theorem RybinAI2026.P01.crossIntegral_double_add_same_numerator
    {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)+B) C*crossIntegral X Y B C+
        crossIntegral X Y ((A+B)+A) C*crossIntegral X Y A C ≤
      crossIntegral X Y A C*crossIntegral X Y B C) ∧
    (crossIntegral X Y C ((A+B)+B)*crossIntegral X Y C B+
        crossIntegral X Y C ((A+B)+A)*crossIntegral X Y C A ≤
      crossIntegral X Y C A*crossIntegral X Y C B) := by
  sorry
Source
Derived fixed-numerator consequence for CUHK-Shenzhen AI Math Problems, Problem 1 (Prof. Cosme Louart), https://rybindmitry.github.io/problems/1.html; obtained from the proved Prove2Me harmonic denominator contraction RybinAI2026.P01.crossIntegral_add_harmonic (b1591757-f2b5-43ce-a2da-99b934101c6e).

View graph