Simultaneous coordinate-permutation invariance of the matrix integral

Proved

RybinAI2026.P01.distance_reindex

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

integral-inequalitymatrix-analysispositive-definite-matrices

For every natural number $n$ , every permutation $\pi$ of the $n$ coordinates, and arbitrary real $n\times n$ matrices $A,B$ , define

A^{\pi}_{ij}=A_{\pi^{-1}(i),\pi^{-1}(j)},\qquad B^{\pi}_{ij}=B_{\pi^{-1}(i),\pi^{-1}(j)}.

For the double spherical integral $d$ defined in Problem 1, with its original unnormalized surface measure,

d(A^{\pi},B^{\pi})=d(A,B).

No symmetry or positive-definiteness hypotheses are required for this identity. The statement concerns the total-valued integral in the original definition, including its convention for nonintegrable functions. The same coordinate permutation is applied to both rows and columns of both matrices. This lemma permits relabeling coordinates in the matrix inequality without changing the distance. Dimension zero is included.

Formalization Note The coordinate transformations use Matrix.reindex in the pinned environment. This is invariance under orthogonal coordinate permutations; it does not assert invariance under arbitrary invertible congruences.

Preamble

import Definitions.Def_rybin2026_p01_matrix_integral

open Matrix RybinAI2026.P01

Formal statement

theorem RybinAI2026.P01.distance_reindex {n : ℕ} (e : Equiv.Perm (Fin n))
    (A B : Matrix (Fin n) (Fin n) ℝ) :
    distance (Matrix.reindex e e A) (Matrix.reindex e e B) = distance A B := by
  sorry

Source

https://rybindmitry.github.io/problems/1.html, definition of d in Problem 1. Derived symmetry lemma. Surface-measure proof uses Mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f, MeasureTheory/Constructions/HaarToSphere.lean (toSphere_apply') and MeasureTheory/Measure/Haar/InnerProductSpace.lean (LinearIsometryEquiv.measurePreserving).

View graph