Problem 01 definitions — Positive definite matrix integral inequality

Definition

rybin2026_p01_matrix_integral

by wenxinzhang · Sep 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

integral-inequalitymatrix-analysispositive-definite-matrices

Euclidean. For every $n\in\mathbb N$ , including $n=0$ , let $I_n=\{0,\ldots,n-1\}$ . The space $\operatorname{Euclidean}(n)$ is the real coordinate space $\mathbb R^{I_n}$ , equipped with the standard Euclidean norm $\lVert x\rVert_2=(\sum_{i\in I_n}|x_i|^2)^{1/2}$ . For $n=0$ , $I_n$ is empty and this space consists only of the zero vector.

surfaceMeasure. For every $n\in\mathbb N$ , let $E_n=\mathbb R^{I_n}$ with its Euclidean norm and let $S_n=\{x\in E_n:\lVert x\rVert_2=1\}$ . The measure $\operatorname{surfaceMeasure}(n)$ is the measure $\sigma_n$ on $S_n$ induced from Lebesgue volume on $E_n$ by its polar-decomposition construction, with no additional normalization to make it a probability measure. When $n=0$ , $S_n$ is empty, so $\sigma_n$ is the unique measure on the empty space.

bilinear. For every $n\in\mathbb N$ , every real matrix $M=(M_{ij})_{i,j\in I_n}$ , and every $u,v\in\mathbb R^{I_n}$ , the quantity $\operatorname{bilinear}(M,u,v)$ is

\sum_{i\in I_n}u_i\left(\sum_{j\in I_n}M_{ij}v_j\right) =\sum_{i,j\in I_n}u_iM_{ij}v_j.

No symmetry, definiteness, or other condition is imposed on $M$ , and no normalization is imposed on $u$ or $v$ . For $n=0$ , both sums are empty and the value is $0$ .

distance. For every $n\in\mathbb N$ , including $n=0$ , and arbitrary real $n\times n$ matrices $A$ and $B$ , let $S_n=\{x\in\mathbb R^{I_n}:\lVert x\rVert_2=1\}$ and let $\sigma_n$ be the sphere measure induced from Lebesgue volume by polar decomposition. The definition assigns the real number

\operatorname{distance}(A,B) = \int_{S_n}\!\left( \int_{S_n} \frac{ \left|\sum_{i,j\in I_n}u_i(A_{ij}-B_{ij})v_j\right| }{ \left(\sum_{i,j\in I_n}u_iA_{ij}u_j\right) \left(\sum_{i,j\in I_n}v_iB_{ij}v_j\right) } \,d\sigma_n(v) \right)d\sigma_n(u).

There are no assumptions that $A$ or $B$ is symmetric, positive, invertible, or distinct. The numerator alone is enclosed in an absolute value; the two quadratic expressions in the denominator are not. Consequently the pointwise quotient can be negative when their product is negative. Real division is total here: if either denominator factor is $0$ , the quotient at that pair $(u,v)$ is defined to be $0$ , regardless of the numerator. Each integral is the real Bochner integral, which is defined to be $0$ when its integrand is not integrable; in particular, a nonintegrable inner integral has value $0$ , and a nonintegrable resulting outer integrand makes the entire outer integral $0$ . For $n=0$ , the unit sphere is empty and the double integral is $0$ .

Definition code

import Mathlib.LinearAlgebra.Matrix.PosDef
import Mathlib.Analysis.Normed.Lp.MeasurableSpace
import Mathlib.MeasureTheory.Constructions.HaarToSphere
import Mathlib.MeasureTheory.Integral.Prod

open Matrix MeasureTheory Metric
open scoped BigOperators

namespace RybinAI2026.P01

/-- Euclidean coordinate space used by the matrix integral problem, equipped with the `ℓ²` norm. -/
abbrev Euclidean (n : ℕ) := EuclideanSpace ℝ (Fin n)

/-- The canonical surface measure obtained from Lebesgue measure by polar decomposition. -/
noncomputable def surfaceMeasure (n : ℕ) : Measure (sphere (0 : Euclidean n) 1) :=
  (volume : Measure (Euclidean n)).toSphere

/-- The bilinear numerator `uᵀ M v`. -/
def bilinear {n : ℕ} (M : Matrix (Fin n) (Fin n) ℝ)
    (u v : Euclidean n) : ℝ :=
  dotProduct (fun i => u i) (M *ᵥ fun j => v j)

/-- The double spherical integral from problem 1.  No normalization is imposed on surface
measure; multiplying the measure by a fixed constant multiplies every occurrence of `distance`
by the same constant and does not affect the target inequality. -/
noncomputable def distance {n : ℕ} (A B : Matrix (Fin n) (Fin n) ℝ) : ℝ :=
  ∫ u, ∫ v,
    |bilinear (A - B) u.1 v.1| /
      (bilinear A u.1 u.1 * bilinear B v.1 v.1)
    ∂surfaceMeasure n ∂surfaceMeasure n

end RybinAI2026.P01

Source

https://rybindmitry.github.io/problems/1.html

Read-back

What the Lean code literally says, in plain math · gpt-5.6-sol

bilinear. For every $n\in\mathbb N$ , every real matrix $M=(M_{ij})_{i,j\in I_n}$ , and every $u,v\in\mathbb R^{I_n}$ , the quantity $\operatorname{bilinear}(M,u,v)$ is

\sum_{i\in I_n}u_i\left(\sum_{j\in I_n}M_{ij}v_j\right) =\sum_{i,j\in I_n}u_iM_{ij}v_j.

No symmetry, definiteness, or other condition is imposed on $M$ , and no normalization is imposed on $u$ or $v$ . For $n=0$ , both sums are empty and the value is $0$ .

\operatorname{distance}(A,B) = \int_{S_n}\!\left( \int_{S_n} \frac{ \left|\sum_{i,j\in I_n}u_i(A_{ij}-B_{ij})v_j\right| }{ \left(\sum_{i,j\in I_n}u_iA_{ij}u_j\right) \left(\sum_{i,j\in I_n}v_iB_{ij}v_j\right) } \,d\sigma_n(v) \right)d\sigma_n(u).

Human review

Endorsed by Shuze Chen · Sep 4, 2026
Endorsed by wenxinzhang · Sep 4, 2026
Confirmed by the mission captain (proposal self-audit).

View graph