Joint continuity of the spherical matrix integral on positive definite pairs

Proved

RybinAI2026.P01.continuousOn_distance

by kptm · Sep 5, 2026 · Mathlib c5ea003 (Lean v4.30.0)

continuityintegral-inequalitymatrix-analysis

For every natural number $n$ , let $P_n$ be the set of real symmetric positive definite $n\times n$ matrices, with the topology of entrywise convergence. Let $\sigma_n$ be the surface measure on the Euclidean unit sphere obtained from Lebesgue measure by polar decomposition, without probability normalization. Define

d_n(A,B)=\int_{S^{n-1}}\int_{S^{n-1}} \frac{|u^{\mathsf T}(A-B)v|}{(u^{\mathsf T}Au)(v^{\mathsf T}Bv)} \,d\sigma_n(v)\,d\sigma_n(u).

Then the map

(A,B)\longmapsto d_n(A,B)

is jointly continuous on $P_n\times P_n$ . In dimension zero the sphere is empty and the integral is zero, so the statement includes $n=0$ .

This continuity lemma is an intermediate result for passing matrix integral inequalities from dense families to arbitrary positive definite matrices. It concerns the integral defined in Problem 1; it does not assume or assert the main addition inequality.

Preamble

import Definitions.Def_rybin2026_p01_matrix_integral

open Matrix

Formal statement

namespace RybinAI2026.P01

theorem continuousOn_distance (n : ℕ) :
    ContinuousOn (fun p : Matrix (Fin n) (Fin n) ℝ × Matrix (Fin n) (Fin n) ℝ =>
      distance p.1 p.2) {p | p.1.PosDef ∧ p.2.PosDef} := by sorry

end RybinAI2026.P01

Source

Derived continuity lemma for the integral in CUHK-Shenzhen AI Math Problems, Problem 1, first displayed formula, https://rybindmitry.github.io/problems/1.html. This is a supporting lemma proved from that definition, not a separately numbered claim in the source. Formal definition: https://prove2.me/theorems/81e3e6fa-5fd2-4e0f-bb54-f5f379792198. The continuity argument follows the community reductions by ryanshin (submission 12a695ea-b6bd-4df8-8293-e655bd22d0f7) and wamlart (20c60eaf-e3d9-40b1-8da3-1f26f4949d37).

View graph