One-sphere L² coefficients for reciprocal quadratic forms

Open

RybinAI2026.P01.one_sphere_l2_coefficients

by Zexuan Liu · Oct 1, 2026 · Mathlib c5ea003 (Lean v4.30.0)

For positive-definite real matrices A and B, there are nonnegative coefficients α and β with α²+β²≤1 such that every absolute linear spherical integral weighted by the reciprocal quadratic form A+B is at most α times the corresponding A-weighted integral and at most β times the corresponding B-weighted integral. This one-sphere lemma is the analytic core of the crossIntegral coefficient theorem: Fubini/Tonelli applies it pointwise in the second sphere variable, and the transposed version gives the second-slot bounds.

Preamble

import Definitions.Def_rybin2026_p01_cross_integral
import Definitions.Def_rybin2026_p01_matrix_integral
set_option autoImplicit false
open Matrix MeasureTheory Metric RybinAI2026.P01
open scoped BigOperators

Formal statement

theorem RybinAI2026.P01.one_sphere_l2_coefficients
    {n : ℕ} (A B : Matrix (Fin n) (Fin n) ℝ)
    (hA : A.PosDef) (hB : B.PosDef) :
    ∃ α β : ℝ, 0 ≤ α ∧ 0 ≤ β ∧ α ^ 2 + β ^ 2 ≤ 1 ∧
      ∀ z : Euclidean n,
        (∫ u : Metric.sphere (0 : Euclidean n) 1, |bilinear (1 : Matrix (Fin n) (Fin n) ℝ) u.1 z| / bilinear (A + B) u.1 u.1 ∂surfaceMeasure n) ≤
          α * (∫ u : Metric.sphere (0 : Euclidean n) 1, |bilinear (1 : Matrix (Fin n) (Fin n) ℝ) u.1 z| / bilinear A u.1 u.1 ∂surfaceMeasure n) ∧
        (∫ u : Metric.sphere (0 : Euclidean n) 1, |bilinear (1 : Matrix (Fin n) (Fin n) ℝ) u.1 z| / bilinear (A + B) u.1 u.1 ∂surfaceMeasure n) ≤
          β * (∫ u : Metric.sphere (0 : Euclidean n) 1, |bilinear (1 : Matrix (Fin n) (Fin n) ℝ) u.1 z| / bilinear B u.1 u.1 ∂surfaceMeasure n) := by
  sorry

Source

Derived analytic core for RybinAI2026.P01.crossIntegral_add_l2_coefficients; crossIntegral is the iterated spherical integral from https://rybindmitry.github.io/problems/1.html

View graph