GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysisrandom_matrixgoe_rotation

The rotation invariance of the GOE

GaussianAnalysis.random_matrix.goe_rotationlibrary/random_matrix/goe_rotation.v722 lines21 lemmas and theorems, 3 definitionssource
Imports 7 library modules and 23 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.algebra.sesquilinear, mathcomp.algebra.interval, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.measurable_realfun, mathcomp.analysis.numfun, mathcomp.analysis.probability_theory.probability

Imported by 2
Required by 5 files of the paper proofs

Let W = goe_mx a, with a of law gauss (n * n). Lemma 5.13 of Koehler and Sohn (arXiv 2608.27372, lines 5820-5860) averages the diagonal of U D U^T over a Haar matrix U, and MathComp-Analysis has no Haar measure on the orthogonal group. Item G6 of phase 5 proves what the paper uses the lemma for, that the diagonal of F(W) is nearly constant for an equivariant F, from the invariance of the law of W under orthogonal conjugation, with Householder reflections in place of the Haar matrix. Every result holds for every n.

  • goe_conj_integral: the law of W is invariant under W |-> Q^T W Q for every orthogonal Q. The map a |-> mxvec (Q^T (vec_mx a) Q) is linear with an orthogonal matrix conj_mx Q (conj_mx_orthogonal: it preserves the Frobenius product, mxdot_conj), Q^T goe_mx a Q = goe_mx (a conj_mx Q) (goe_mx_conj), and gauss (n * n) is invariant under orthogonal maps (integral_gauss_mulmx).
  • goe_equiv_form: for F equivariant (conj_equivariant) and every unit row vector u, u F(W) u^T has the law of F(W)_00, because the Householder reflection that maps the first basis vector to u^T (householder_swap) conjugates W into a matrix of the same law. Hence each diagonal entry of F(W) has the law of F(W)_00 (goe_equiv_diag), and so has (F(W)_ii + F(W)_jj) / 2 + s F(W)_ij for i != j and s = 1 or -1 when F(W) is symmetric (goe_equiv_pair, with u = (e_i + s e_j) / sqrt 2).
  • goe_diag_var_identity: if moreover F(W) is symmetric and E F(W)_ij^2 is finite, then E[F(W)_ii F(W)_jj] + 2 E[F(W)_ij^2] = E[F(W)_00^2] for i != j (goe_equiv_pair2), hence E[diag_var F(W)] = 2 / (n + 2) E[|F(W)|_F^2 / n - (tr F(W) / n)^2]. This is the identity of the proof of Lemma 5.13 (lines 5853-5860), where the rho_i are the eigenvalues of F(W).
  • goe_diag_var_tail: for C >= 0 and eps > 0, P(diag_var F(W) >= eps) <= 2 C / ((n + 2) eps) + P(|F(W)|_F^2 > C n), by the identity for the map W |-> F(W) when |F(W)|_F^2 <= C n and 0 otherwise, which is still equivariant, and Markov's inequality (gauss_markov). So diag_var F(W) tends to 0 in probability when |F(W)|_F^2 / n is bounded in probability, as for F(W) the positive part (psd_part of matrix/psd_part.v) of W - w I with w bounded, which is how Proposition 5.15 uses Lemma 5.13.
conj_equivariant FF (Q W Q^T) = Q F(W) Q^T for every orthogonal Q and every symmetric W
diag_var A(1 / n) \sum_j (A_jj - tr A / n)^2, the empirical variance of the diagonal of A : 'M_n

Main results

ResultsStatement
goe_conj_integralgoe_equiv_formconj_equivariant
The law of the GOE matrix W is invariant under W |-> Q^T W Q for every orthogonal Q. For F equivariant (F (Q W Q^T) = Q F(W) Q^T for every orthogonal Q and symmetric W) and every unit row vector u, u F(W) u^T has the law of F(W)_00: a Householder reflection maps the first basis vector to u.
goe_diag_var_identitygoe_diag_var_taildiag_var
Lemma 5.13 of Koehler and Sohn without the Haar measure. For F equivariant with F(W) symmetric and E F(W)_ij^2 finite, E[diag_var F(W)] = 2 / (n + 2) E[|F(W)|_F^2 / n - (tr F(W) / n)^2], where diag_var A is the empirical variance of the diagonal of A. Without moment assumptions, P(diag_var F(W) >= eps) <= 2 C / ((n + 2) eps) + P(|F(W)|_F^2 > C n) for every C >= 0 and eps > 0.

Declarations24 exported, 12 local

lemma, theoremdefinitioninstancelocal
sectiongoe_invariance
Context {R : realType} (d : nat).
definition conj_mx source, line 74
Type
forall {R : realType} [d : nat], 'M_d -> 'M_(d * d)
Definition
Definition conj_mx (Q : 'M[R]_d) : 'M[R]_(d * d) :=
  lin_mx (mulmxr Q \o mulmx Q^T).

The matrix of a |-> mxvec (Q^T (vec_mx a) Q).

Used by 4 declarations in 1 file
lemma conj_mxE source, line 77 
forall {R : realType} [d : nat] (Q : 'M_d) (a : 'rV_(d * d)),
a *m conj_mx Q = mxvec (Q^T *m vec_mx a *m Q)
Statement as written in the source
Lemma conj_mxE (Q : 'M[R]_d) (a : 'rV[R]_(d * d)) :
  a *m conj_mx Q = mxvec (Q^T *m vec_mx a *m Q).
Used by 2 declarations in 1 file
let mxdot_vec section-local source, line 82 
Let mxdot_vec (A B : 'M[R]_d) : mxdot (mxvec A) (mxvec B) = mxdot A B.

mxvec is an isometry for the Frobenius product.

Used by 1 declaration in 1 file
lemma mxdot_conj source, line 90 
forall {R : realType} [d : nat] [Q : 'M_d] (A B : 'M_d),
Q \is orthogonalmx -> mxdot (Q^T *m A *m Q) (Q^T *m B *m Q) = mxdot A B

Conjugation by an orthogonal matrix preserves the Frobenius product.

Statement as written in the source
Lemma mxdot_conj (Q A B : 'M[R]_d) : Q \is orthogonalmx ->
  mxdot (Q^T *m A *m Q) (Q^T *m B *m Q) = mxdot A B.
Used by 1 declaration in 1 file
lemma conj_mx_orthogonal source, line 98 
forall {R : realType} [d : nat] [Q : 'M_d],
Q \is orthogonalmx -> conj_mx Q \is orthogonalmx
Statement as written in the source
Lemma conj_mx_orthogonal (Q : 'M[R]_d) : Q \is orthogonalmx ->
  conj_mx Q \is orthogonalmx.
Used by 1 declaration in 1 file
lemma goe_mx_conj source, line 109 
forall {R : realType} [d : nat] (Q : 'M_d) (a : 'rV_(d * d)),
Q^T *m goe_mx a *m Q = goe_mx (a *m conj_mx Q)
Statement as written in the source
Lemma goe_mx_conj (Q : 'M[R]_d) (a : 'rV[R]_(d * d)) :
  Q^T *m goe_mx a *m Q = goe_mx (a *m conj_mx Q).
Used by 1 declaration in 1 file
lemma measurable_goe_mx source, line 116 
forall {R : realType} [d : nat], measurable_fun [set: 'rV_(d * d)] (goe_mx (d:=d))
Statement as written in the source
Lemma measurable_goe_mx : measurable_fun [set: 'rV[R]_(d * d)] (@goe_mx R d).
Used by 2 declarations in 2 files
theorem goe_conj_integral main result source, line 124 
forall {R : realType} [d : nat] [Q : 'M_d] [F : 'M_d -> \bar R],
Q \is orthogonalmx ->
measurable_fun [set: 'rV_(d * d)]
  (fun a : 'rV_(d * d) =>
   F (goe_mx a)) ->
(\int[gauss (d * d)]_a F (Q^T *m goe_mx a *m Q))%E = (\int[gauss (d * d)]_a F (goe_mx a))%E

The law of the GOE is invariant under conjugation by an orthogonal matrix: Q^T W Q has the law of W.

Main result, as the README states it

The law of the GOE matrix W is invariant under W |-> Q^T W Q for every orthogonal Q. For F equivariant (F (Q W Q^T) = Q F(W) Q^T for every orthogonal Q and symmetric W) and every unit row vector u, u F(W) u^T has the law of F(W)_00: a Householder reflection maps the first basis vector to u.

Statement as written in the source
Theorem goe_conj_integral (Q : 'M[R]_d) (F : 'M[R]_d -> \bar R) :
  Q \is orthogonalmx ->
  measurable_fun [set: 'rV[R]_(d * d)] (fun a => F (goe_mx a)) ->
  (\int[gauss (d * d)]_a F (Q^T *m goe_mx a *m Q) =
   \int[gauss (d * d)]_a F (goe_mx a))%E.
Used by 1 declaration in 1 file
sectiondiag_var
Context {R : realType}.
Implicit Types n : nat.
definition conj_equivariant main result source, line 147
Type
forall {R : realType} [n : nat], ('M_n -> 'M_n) -> Prop
Definition
Definition conj_equivariant n (F : 'M[R]_n -> 'M[R]_n) : Prop :=
  forall Q W : 'M[R]_n, Q \is orthogonalmx -> W \is symmetricmx ->
  F (Q *m W *m Q^T) = Q *m F W *m Q^T.

F commutes with the conjugations by orthogonal matrices on the symmetric matrices, as the spectral functions P^T diag(d) P |-> P^T diag(f (d_i)) P do.

Main result

Stated in the README together with goe_conj_integral.

Used by 1 declaration in 1 file
definition diag_var main result source, line 152
Type
forall {R : realType} [n : nat], 'M_n -> R
Definition
Definition diag_var n (A : 'M[R]_n) : R :=
  n%:R^-1 * \sum_j (A j j - \tr A / n%:R) ^+ 2.

The empirical variance of the diagonal entries of A.

Main result

Stated in the README together with goe_diag_var_identity.

Used by 5 declarations in 1 file
lemma diag_var_ge0 source, line 155 
forall {R : realType} [n : nat] (A : 'M_n), 0 <= diag_var A
Statement as written in the source
Lemma diag_var_ge0 n (A : 'M[R]_n) : 0 <= diag_var A.
Used by 2 declarations in 1 file
lemma diag_varE source, line 161 
forall {R : realType} [n : nat] (A : 'M_n),
diag_var A = n%:R^-1 * \sum_j A j j ^+ 2 - (\tr A / n%:R) ^+ 2
Statement as written in the source
Lemma diag_varE n (A : 'M[R]_n) :
  diag_var A = n%:R^-1 * \sum_j A j j ^+ 2 - (\tr A / n%:R) ^+ 2.
Used by 3 declarations in 1 file
lemma diag_sqr_le source, line 175 
forall {R : realType} [n : nat] (A : 'M_n), \sum_j A j j ^+ 2 <= mxdot A A
Statement as written in the source
Lemma diag_sqr_le n (A : 'M[R]_n) : \sum_j A j j ^+ 2 <= mxdot A A.
Used by 2 declarations in 1 file
lemma trace_sqr_le source, line 182 
forall {R : realType} [n : nat] (A : 'M_n), (\tr A / n%:R) ^+ 2 <= mxdot A A / n%:R

(tr A / n)^2 <= |A|_F^2 / n.

Statement as written in the source
Lemma trace_sqr_le n (A : 'M[R]_n) : (\tr A / n%:R) ^+ 2 <= mxdot A A / n%:R.
Used by 1 declaration in 1 file
sectiongauss_markov
Context {R : realType} (m : nat).
lemma gauss_markov source, line 194 
forall {R : realType} [m : nat] [f : 'rV_m -> R] [c : R],
0 < c ->
measurable_fun [set: 'rV_m] f ->
(forall x : 'rV_m, 0 <= f x) ->
(gauss m).-integrable [set: 'rV_m] (EFin \o f) ->
(gauss m [set x | (c <= f x)%R] <= (c^-1 * \int[gauss m]_x f x)%:E)%E

Markov's inequality: P(f >= c) <= E f / c for f >= 0 and c > 0.

Statement as written in the source
Lemma gauss_markov (f : 'rV[R]_m -> R) (c : R) : 0 < c ->
  measurable_fun [set: 'rV[R]_m] f -> (forall x, 0 <= f x) ->
  (gauss m).-integrable [set: 'rV[R]_m] (EFin \o f) ->
  (gauss m [set x | (c <= f x)%R] <= (c^-1 * \int[gauss m]_x f x)%:E)%E.
Used by 1 declaration in 1 file
sectiongoe_equivariant
Context {R : realType} (d : nat).
Local Notation N := d.+1.
Variable F : 'M[R]_N -> 'M[R]_N.
Hypothesis Feq : conj_equivariant F.
Hypothesis Fm : measurable_fun [set: 'rV[R]_(N * N)] (fun a => F (goe_mx a)).
lemma mulmx_delta_entry0 source, line 231 
forall {R : realType} [d : nat] (X : 'M_d.+1) (i j : 'I_d.+1),
('e_i *m X *m delta_mx j 0 : 'cV_1) 0 0 = X i j
Statement as written in the source
Lemma mulmx_delta_entry0 (X : 'M[R]_N) (i j : 'I_N) :
  (delta_mx 0 i *m X *m delta_mx j 0 : 'M[R]_1) 0 0 = X i j.
Used by 2 declarations in 1 file
lemma goe_equiv_form main result source, line 237 
forall {R : realType} [d : nat] [F : 'M_d.+1 -> 'M_d.+1],
conj_equivariant F ->
measurable_fun [set: 'rV_(d.+1 * d.+1)]
  (fun a : 'rV_(d.+1 * d.+1) =>
   F (goe_mx a)) ->
forall [u : 'rV_d.+1] [phi : R -> \bar R],
mxdot u u = 1 ->
measurable_fun [set: R] phi ->
(\int[gauss (d.+1 * d.+1)]_a phi ((u *m F (goe_mx a) *m u^T) ord0 ord0))%E =
(\int[gauss (d.+1 * d.+1)]_a phi (F (goe_mx a) ord0 ord0))%E

For every unit vector u, u F(W) u^T has the law of F(W)_00: a Householder reflection maps the first basis vector to u.

Main result

Stated in the README together with goe_conj_integral.

Statement as written in the source
Lemma goe_equiv_form (u : 'rV[R]_N) (phi : R -> \bar R) :
  mxdot u u = 1 -> measurable_fun [set: R] phi ->
  (\int[gauss (N * N)%N]_a phi ((u *m F (goe_mx a) *m u^T) ord0 ord0) =
   \int[gauss (N * N)%N]_a phi (F (goe_mx a) ord0 ord0))%E.
Used by 1 declaration in 1 file
lemma goe_equiv_formR source, line 263 
forall {R : realType} [d : nat] [F : 'M_d.+1 -> 'M_d.+1],
conj_equivariant F ->
measurable_fun [set: 'rV_(d.+1 * d.+1)]
  (fun a : 'rV_(d.+1 * d.+1) =>
   F (goe_mx a)) ->
forall [u : 'rV_d.+1] [phi : R -> R],
mxdot u u = 1 ->
measurable_fun [set: R] phi ->
\int[gauss (d.+1 * d.+1)]_a phi ((u *m F (goe_mx a) *m u^T) ord0 ord0) =
\int[gauss (d.+1 * d.+1)]_a phi (F (goe_mx a) ord0 ord0)
Statement as written in the source
Lemma goe_equiv_formR (u : 'rV[R]_N) (phi : R -> R) :
  mxdot u u = 1 -> measurable_fun [set: R] phi ->
  \int[gauss (N * N)%N]_a phi ((u *m F (goe_mx a) *m u^T) ord0 ord0) =
  \int[gauss (N * N)%N]_a phi (F (goe_mx a) ord0 ord0).
Used by 2 declarations in 1 file
lemma goe_equiv_diag source, line 273 
forall {R : realType} [d : nat] [F : 'M_d.+1 -> 'M_d.+1],
conj_equivariant F ->
measurable_fun [set: 'rV_(d.+1 * d.+1)]
  (fun a : 'rV_(d.+1 * d.+1) =>
   F (goe_mx a)) ->
forall (i : 'I_d.+1) [phi : R -> R],
measurable_fun [set: R] phi ->
\int[gauss (d.+1 * d.+1)]_a phi (F (goe_mx a) i i) =
\int[gauss (d.+1 * d.+1)]_a phi (F (goe_mx a) ord0 ord0)

The diagonal entries of F(W) have the law of F(W)_00.

Statement as written in the source
Lemma goe_equiv_diag (i : 'I_N) (phi : R -> R) : measurable_fun [set: R] phi ->
  \int[gauss (N * N)%N]_a phi (F (goe_mx a) i i) =
  \int[gauss (N * N)%N]_a phi (F (goe_mx a) ord0 ord0).
Used by 1 declaration in 1 file
Hypothesis Fsym : forall W : 'M[R]_N, W \is symmetricmx -> F W \is symmetricmx.
lemma goe_equiv_pair source, line 287 
forall {R : realType} [d : nat] [F : 'M_d.+1 -> 'M_d.+1],
conj_equivariant F ->
measurable_fun [set: 'rV_(d.+1 * d.+1)]
  (fun a : 'rV_(d.+1 * d.+1) =>
   F (goe_mx a)) ->
(forall W : 'M_d.+1, W \is symmetricmx -> F W \is symmetricmx) ->
forall [i j : 'I_d.+1] [s : R] [phi : R -> R],
i != j ->
s ^+ 2 = 1 ->
measurable_fun [set: R] phi ->
\int[gauss (d.+1 * d.+1)]_a
   phi ((F (goe_mx a) i i + F (goe_mx a) j j) / 2 + s * F (goe_mx a) i j) =
\int[gauss (d.+1 * d.+1)]_a phi (F (goe_mx a) ord0 ord0)

For i != j and s = 1 or s = -1, (F(W)_ii + F(W)_jj) / 2 + s F(W)_ij has the law of F(W)_00: take u = (e_i + s e_j) / sqrt 2.

Statement as written in the source
Lemma goe_equiv_pair (i j : 'I_N) (s : R) (phi : R -> R) :
  i != j -> s ^+ 2 = 1 -> measurable_fun [set: R] phi ->
  \int[gauss (N * N)%N]_a
    phi ((F (goe_mx a) i i + F (goe_mx a) j j) / 2 + s * F (goe_mx a) i j) =
  \int[gauss (N * N)%N]_a phi (F (goe_mx a) ord0 ord0).
Used by 1 declaration in 1 file
Hypothesis Fi : forall i j : 'I_N,
  (gauss (N * N)).-integrable [set: 'rV[R]_(N * N)]
    (EFin \o (fun a => F (goe_mx a) i j ^+ 2)).
Local Notation qint f :=
  ((gauss (N * N)).-integrable [set: 'rV[R]_(N * N)] (EFin \o f)).
let mX section-local source, line 322 
Let mX (i j : 'I_N) :
  measurable_fun [set: 'rV[R]_(N * N)] (fun a => F (goe_mx a) i j).
let qintD section-local source, line 326 
Let qintD (f g : 'rV[R]_(N * N) -> R) : qint f -> qint g ->
  qint (fun a => f a + g a).
Used by 3 declarations in 1 file
let qintZ section-local source, line 334 
Let qintZ (k : R) (f : 'rV[R]_(N * N) -> R) : qint f -> qint (fun a => k * f a).
Used by 1 declaration in 1 file
let qintB section-local source, line 341 
Let qintB (f g : 'rV[R]_(N * N) -> R) : qint f -> qint g ->
  qint (fun a => f a - g a).
let qint_sum section-local source, line 350 
Let qint_sum (I : Type) (s : seq I) (f : I -> 'rV[R]_(N * N) -> R) :
  (forall i, qint (f i)) -> qint (fun a => \sum_(i <- s) f i a).
Used by 2 declarations in 1 file
let qintXX section-local source, line 363 
Let qintXX (i j k l : 'I_N) :
  qint (fun a => F (goe_mx a) i j * F (goe_mx a) k l).
Used by 2 declarations in 1 file
let Rint_sum2 section-local source, line 376 
Let Rint_sum2 (f : 'I_N -> 'I_N -> 'rV[R]_(N * N) -> R) :
  (forall i j, qint (f i j)) ->
  \int[gauss (N * N)%N]_a (\sum_i \sum_j f i j a) =
  \sum_i \sum_j \int[gauss (N * N)%N]_a f i j a.
Used by 1 declaration in 1 file
let RintD section-local source, line 389 
Let RintD (f g : 'rV[R]_(N * N) -> R) : qint f -> qint g ->
  \int[gauss (N * N)%N]_a (f a + g a) =
  \int[gauss (N * N)%N]_a f a + \int[gauss (N * N)%N]_a g a.
Used by 1 declaration in 1 file
let RintB section-local source, line 394 
Let RintB (f g : 'rV[R]_(N * N) -> R) : qint f -> qint g ->
  \int[gauss (N * N)%N]_a (f a - g a) =
  \int[gauss (N * N)%N]_a f a - \int[gauss (N * N)%N]_a g a.
Used by 1 declaration in 1 file
let RintZ section-local source, line 399 
Let RintZ (k : R) (f : 'rV[R]_(N * N) -> R) : qint f ->
  \int[gauss (N * N)%N]_a (k * f a) = k * \int[gauss (N * N)%N]_a f a.
Used by 2 declarations in 1 file
let msq section-local source, line 403 
Let msq : measurable_fun [set: R] (fun x : R => x ^+ 2).
Used by 2 declarations in 1 file
lemma goe_equiv_diag2 source, line 407 
forall {R : realType} [d : nat] [F : 'M_d.+1 -> 'M_d.+1],
conj_equivariant F ->
measurable_fun [set: 'rV_(d.+1 * d.+1)]
  (fun a : 'rV_(d.+1 * d.+1) =>
   F (goe_mx a)) ->
forall i : 'I_d.+1,
\int[gauss (d.+1 * d.+1)]_a (F (goe_mx a) i i * F (goe_mx a) i i) =
\int[gauss (d.+1 * d.+1)]_a F (goe_mx a) ord0 ord0 ^+ 2

E[F(W)_ij^2] and E[F(W)_ii F(W)_jj] in terms of c0 = E[F(W)_00^2].

Statement as written in the source
Lemma goe_equiv_diag2 (i : 'I_N) :
  \int[gauss (N * N)%N]_a (F (goe_mx a) i i * F (goe_mx a) i i) =
  \int[gauss (N * N)%N]_a F (goe_mx a) ord0 ord0 ^+ 2.
Used by 2 declarations in 1 file
lemma goe_equiv_pair2 source, line 415 
forall {R : realType} [d : nat] [F : 'M_d.+1 -> 'M_d.+1],
conj_equivariant F ->
measurable_fun [set: 'rV_(d.+1 * d.+1)]
  (fun a : 'rV_(d.+1 * d.+1) =>
   F (goe_mx a)) ->
(forall W : 'M_d.+1, W \is symmetricmx -> F W \is symmetricmx) ->
(forall i j : 'I_d.+1,
 (gauss (d.+1 * d.+1)).-integrable [set: 'rV_(d.+1 * d.+1)]
   (EFin \o (fun a : 'rV_(d.+1 * d.+1) => F (goe_mx a) i j ^+ 2))) ->
forall [i j : 'I_d.+1],
i != j ->
\int[gauss (d.+1 * d.+1)]_a (F (goe_mx a) i i * F (goe_mx a) j j) +
2 * \int[gauss (d.+1 * d.+1)]_a (F (goe_mx a) i j * F (goe_mx a) i j) =
\int[gauss (d.+1 * d.+1)]_a F (goe_mx a) ord0 ord0 ^+ 2
Statement as written in the source
Lemma goe_equiv_pair2 (i j : 'I_N) : i != j ->
  \int[gauss (N * N)%N]_a (F (goe_mx a) i i * F (goe_mx a) j j) +
  2 * \int[gauss (N * N)%N]_a (F (goe_mx a) i j * F (goe_mx a) i j) =
  \int[gauss (N * N)%N]_a F (goe_mx a) ord0 ord0 ^+ 2.
Used by 1 declaration in 1 file
theorem goe_diag_var_identityS source, line 461 
forall {R : realType} [d : nat] [F : 'M_d.+1 -> 'M_d.+1],
conj_equivariant F ->
measurable_fun [set: 'rV_(d.+1 * d.+1)]
  (fun a : 'rV_(d.+1 * d.+1) =>
   F (goe_mx a)) ->
(forall W : 'M_d.+1, W \is symmetricmx -> F W \is symmetricmx) ->
(forall i j : 'I_d.+1,
 (gauss (d.+1 * d.+1)).-integrable [set: 'rV_(d.+1 * d.+1)]
   (EFin \o (fun a : 'rV_(d.+1 * d.+1) => F (goe_mx a) i j ^+ 2))) ->
\int[gauss (d.+1 * d.+1)]_a diag_var (F (goe_mx a)) =
2 / (d.+1%:R + 2) *
\int[gauss (d.+1 * d.+1)]_a
   (mxdot (F (goe_mx a)) (F (goe_mx a)) / d.+1%:R - (\tr (F (goe_mx a)) / d.+1%:R) ^+ 2)

Lemma 5.13 of Koehler and Sohn without the Haar measure, for N = d + 1.

Statement as written in the source
Theorem goe_diag_var_identityS :
  \int[gauss (N * N)%N]_a diag_var (F (goe_mx a)) =
  2 / (N%:R + 2) * \int[gauss (N * N)%N]_a
    (mxdot (F (goe_mx a)) (F (goe_mx a)) / N%:R -
     (\tr (F (goe_mx a)) / N%:R) ^+ 2).
Used by 1 declaration in 1 file
sectiongoe_diag
Context {R : realType} (n : nat).
Variable F : 'M[R]_n -> 'M[R]_n.
Hypothesis Feq : conj_equivariant F.
Hypothesis Fsym : forall W : 'M[R]_n, W \is symmetricmx -> F W \is symmetricmx.
Hypothesis Fm : measurable_fun [set: 'rV[R]_(n * n)] (fun a => F (goe_mx a)).
theorem goe_diag_var_identity main result source, line 555 
forall {R : realType} [n : nat] [F : 'M_n -> 'M_n],
conj_equivariant F ->
(forall W : 'M_n, W \is symmetricmx -> F W \is symmetricmx) ->
measurable_fun [set: 'rV_(n * n)]
  (fun a : 'rV_(n * n) =>
   F (goe_mx a)) ->
(forall i j : 'I_n,
 (gauss (n * n)).-integrable [set: 'rV_(n * n)]
   (EFin \o (fun a : 'rV_(n * n) => F (goe_mx a) i j ^+ 2))) ->
\int[gauss (n * n)]_a diag_var (F (goe_mx a)) =
2 / (n%:R + 2) *
\int[gauss (n * n)]_a
   (mxdot (F (goe_mx a)) (F (goe_mx a)) / n%:R - (\tr (F (goe_mx a)) / n%:R) ^+ 2)

Lemma 5.13 of Koehler and Sohn, with the GOE instead of a Haar matrix: for F equivariant and E |F(W)|_F^2 finite, the diagonal of F(W) has E[diag_var F(W)] = 2 / (n + 2) E[|F(W)|_F^2 / n - (tr F(W) / n)^2].

Main result, as the README states it

Lemma 5.13 of Koehler and Sohn without the Haar measure. For F equivariant with F(W) symmetric and E F(W)_ij^2 finite, E[diag_var F(W)] = 2 / (n + 2) E[|F(W)|_F^2 / n - (tr F(W) / n)^2], where diag_var A is the empirical variance of the diagonal of A. Without moment assumptions, P(diag_var F(W) >= eps) <= 2 C / ((n + 2) eps) + P(|F(W)|_F^2 > C n) for every C >= 0 and eps > 0.

Statement as written in the source
Theorem goe_diag_var_identity :
  (forall i j : 'I_n, (gauss (n * n)).-integrable [set: 'rV[R]_(n * n)]
     (EFin \o (fun a => F (goe_mx a) i j ^+ 2))) ->
  \int[gauss (n * n)%N]_a diag_var (F (goe_mx a)) =
  2 / (n%:R + 2) * \int[gauss (n * n)%N]_a
    (mxdot (F (goe_mx a)) (F (goe_mx a)) / n%:R -
     (\tr (F (goe_mx a)) / n%:R) ^+ 2).
Used by 1 declaration in 1 file
sectiongoe_diag_tail
Context {R : realType} (n : nat).
Variable F : 'M[R]_n -> 'M[R]_n.
Hypothesis Feq : conj_equivariant F.
Hypothesis Fsym : forall W : 'M[R]_n, W \is symmetricmx -> F W \is symmetricmx.
Hypothesis Fm : measurable_fun [set: 'rV[R]_(n * n)] (fun a => F (goe_mx a)).
theorem goe_diag_var_tail main result source, line 586 
forall {R : realType} [n : nat] [F : 'M_n -> 'M_n],
conj_equivariant F ->
(forall W : 'M_n, W \is symmetricmx -> F W \is symmetricmx) ->
measurable_fun [set: 'rV_(n * n)]
  (fun a : 'rV_(n * n) =>
   F (goe_mx a)) ->
forall [C eps : R],
0 <= C ->
0 < eps ->
(gauss (n * n) [set a | (eps <= diag_var (F (goe_mx a)))%R] <=
 (2 * C / ((n%:R + 2) * eps))%:E +
 gauss (n * n) [set a | (C * n%:R < mxdot (F (goe_mx a)) (F (goe_mx a)))%R])%E

The diagonal of F(W) is nearly constant: for C >= 0 and eps > 0, P(diag_var F(W) >= eps) <= 2 C / ((n + 2) eps) + P(|F(W)|_F^2 > C n). The second term is small when |F(W)|_F^2 / n is bounded in probability, as for the positive part of W - w I with w bounded.

Main result

Stated in the README together with goe_diag_var_identity.

Statement as written in the source
Theorem goe_diag_var_tail (C eps : R) : 0 <= C -> 0 < eps ->
  (gauss (n * n) [set a | (eps <= diag_var (F (goe_mx a)))%R] <=
   (2 * C / ((n%:R + 2) * eps))%:E +
   gauss (n * n)
     [set a | (C * n%:R < mxdot (F (goe_mx a)) (F (goe_mx a)))%R])%E.
Generated from commit 9046883 (tag phase12) of the ellipsoid fitting repository. Signatures are printed by Rocq 9.1.1; links in the source statements come from the compiled .glob files. The source links open the files on GitHub at this commit, in the now-public repository.