GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysisrandom_matrixmatrix_series

Gaussian matrix series

GaussianAnalysis.random_matrix.matrix_serieslibrary/random_matrix/matrix_series.v746 lines34 lemmas and theorems, 1 definitionsource
Imports 11 library modules and 27 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.archimedean, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.algebra.interval, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.sequences, mathcomp.analysis.derive, mathcomp.analysis.exp, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.numfun, mathcomp.analysis.measurable_realfun, mathcomp.analysis.probability_theory.probability, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic

Imported by 2

For matrices H_1, ..., H_r in 'M[R]_n and g of law gauss r, the Gaussian matrix series X = \sum_j g_j H_j (written \sum_j g 0 j *: H j) has trace moments bounded by its variance S = \sum_j H_j^2 alone: no dimension of the matrices enters the bounds. Through the symmetric dilation of rectangular matrices, the same holds for the operator norm of \sum_j g_j B_j.

This file is a Rocq formalization of the credited argument of Lemma 4.2, 'A Gaussian matrix estimate', of 'Pointwise convergence of fourfold ergodic averages for mixing transformations' (OpenAI, 4 October 2026), family 154 of the OpenAI math collection at revision 1581d4cbd. The same lemma is in the section 'Tensor packing' of its companion 'Pointwise Multiple Ergodic Averages for Mixing Transformations'. There is no Lean version. The formalization differs from the manuscript in four points:

  • the recursion holds for every q, and the manuscript states it for q >= 2;
  • the trace inequality uses x^a y^b + y^a x^b <= x^(a+b) + y^(a+b) for x, y >= 0, where the manuscript uses the weighted arithmetic-geometric mean;
  • the hypotheses opnorm S <= sqrt d and tr S <= 2 d on the dilation S are stated on its two diagonal blocks, \sum_j B_j B_j^T and \sum_j B_j^T B_j;
  • the constant of the last bound is explicit, 5, with q = floor (ln (2 + d)) + 1, where the manuscript takes q >= 2 comparable to log (2 + d).

Proved:

  • mxtrace_sandwich_le: |tr (K A^a K A^b)| <= tr (K^2 A^(a+b)) for K, A symmetric and a + b even, in an eigenbasis of A; mxtrace_mul_psd_le: tr (S T) <= opnorm S tr T for T positive semidefinite.
  • moment_root_le, moment_root_powR: E f <= (E f^(k+1))^(1/(k+1)) for a measurable f >= 0 and a probability, the integrals in the extended reals, from Young's inequality with integer exponents (young_exprn).
  • gauss_mx_series_ibp: E tr X^(k+1) = \sum_j E tr (H_j D_j), where D_j = mxpow_deriv X H_j k is the derivative of X^k along H_j, by Gaussian integration by parts in each coordinate (gauss_ibp_polyfun, is_derive_mxpow); gauss_mx_series_trace_sqr: E tr X^2 = tr S.
  • gauss_mx_series_trace_rec: for H_j symmetric, E tr X^(2q+2) <= (2q + 1) opnorm S E tr X^(2q).
  • gauss_mx_series_moment: for H_j symmetric and q >= 1, E tr X^(2q) <= (2q - 1)!! opnorm S^(q-1) tr S, with (2q - 1)!! = \prod_(i < q) (2i + 1), the integral in the extended reals.
  • sym_dilation B is symmetric, linear in B, with square block_mx (B B^T) 0 0 (B^T B), and opnorm B <= opnorm (sym_dilation B); opnorm_block_diag_le: the operator norm of block_mx A 0 0 D is at most the larger of opnorm A and opnorm D.
  • gauss_mx_series_opnorm_moment, gauss_mx_series_opnorm: for B_j in 'M[R]_(m, p) and q >= 1, E opnorm (\sum_j g_j B_j)^(2q) <= (2q - 1)!! sigma^(2(q-1)) tau, hence E opnorm (\sum_j g_j B_j) <= ((2q - 1)!! sigma^(2(q-1)) tau)^(1/(2q)), where sigma^2 = max (opnorm (\sum_j B_j B_j^T), opnorm (\sum_j B_j^T B_j)) and tau = 2 tr (\sum_j B_j B_j^T).
  • gauss_mx_series_opnorm_log: if opnorm (\sum_j B_j B_j^T) and opnorm (\sum_j B_j^T B_j) are at most sqrt d and tr (\sum_j B_j B_j^T) <= d for a real d >= 1, then E opnorm (\sum_j g_j B_j) <= 5 d^(1/4) sqrt (ln (2 + d)).
sym_dilation Bthe symmetric matrix [[0, B], [B^T, 0]] of size m + p of B : 'M[R]_(m, p)

Main results

ResultsStatement
gauss_mx_series_momentgauss_mx_series_trace_recgauss_mx_series_ibpgauss_mx_series_trace_sqr
Gaussian matrix series. For symmetric H_1, ..., H_r in 'M[R]_n, S = \sum_j H_j^2 and g of law gauss r, the series X = \sum_j g_j H_j satisfies E tr X^(2q) <= (2q - 1)!! opnorm S^(q-1) tr S for every q >= 1, with no dimension in the bound (an integral in the extended reals). It follows from E tr X^2 = tr S, which needs no symmetry, and the recursion E tr X^(2q+2) <= (2q + 1) opnorm S E tr X^(2q). The recursion comes from Gaussian integration by parts in each coordinate, E tr X^(k+1) = \sum_j E tr (H_j D_j) with D_j the derivative of X^k along H_j. Lemma 4.2 of the fourfold ergodic paper of family 154 of the OpenAI math collection (revision 1581d4cbd).
gauss_mx_series_opnormgauss_mx_series_opnorm_momentgauss_mx_series_opnorm_log
For B_1, ..., B_r in 'M[R]_(m, p) and g of law gauss r, with sigma^2 = max (opnorm (\sum_j B_j B_j^T), opnorm (\sum_j B_j^T B_j)) and tau = 2 tr (\sum_j B_j B_j^T): E opnorm (\sum_j g_j B_j)^(2q) <= (2q - 1)!! sigma^(2(q-1)) tau and E opnorm (\sum_j g_j B_j) <= ((2q - 1)!! sigma^(2(q-1)) tau)^(1/(2q)) for every q >= 1, through the symmetric dilation sym_dilation B_j = [[0, B_j], [B_j^T, 0]]. If the two operator norms are at most sqrt d and tr (\sum_j B_j B_j^T) <= d for a real d >= 1, then E opnorm (\sum_j g_j B_j) <= 5 d^(1/4) sqrt (ln (2 + d)). No dimension of the matrices enters.
mxtrace_sandwich_lemxtrace_mul_psd_lemoment_root_lemoment_root_powR
|tr (K A^a K A^b)| <= tr (K^2 A^(a+b)) for symmetric K and A and a + b even. tr (S T) <= opnorm S tr T for T positive semidefinite (psdmx T) and any square S. For a probability P, a measurable f >= 0 and k >= 0, E f <= (E f^(k+1))^(1/(k+1)), the expectations being integrals in the extended reals, and E f^(k+1) <= t^(k+1) with t > 0 gives E f <= t.

Declarations35 exported

lemma, theoremdefinitioninstancelocal
sectiontrace_inequalities
Context {R : realType} {n : nat}.
lemma exprn_cross_le source, line 98 
forall {R : realType} [x y : R] (a b : nat),
0 <= x -> 0 <= y -> x ^+ a * y ^+ b + y ^+ a * x ^+ b <= x ^+ (a + b) + y ^+ (a + b)

x^a y^b + y^a x^b <= x^(a+b) + y^(a+b) for x, y >= 0, since (x^a - y^a) (x^b - y^b) >= 0.

Statement as written in the source
Lemma exprn_cross_le (x y : R) a b : 0 <= x -> 0 <= y ->
  x ^+ a * y ^+ b + y ^+ a * x ^+ b <= x ^+ (a + b) + y ^+ (a + b).
Used by 1 declaration in 1 file
lemma mxtrace_diag_sandwich source, line 110 
forall {R : realType} {n : nat} (C : 'M_n) (x y : 'rV_n),
\tr (C *m diag_mx x *m C *m diag_mx y) = \sum_u \sum_v C u v * C v u * (x 0 v * y 0 u)
Statement as written in the source
Lemma mxtrace_diag_sandwich (C : 'M[R]_n) (x y : 'rV[R]_n) :
  \tr (C *m diag_mx x *m C *m diag_mx y) =
  \sum_u \sum_v C u v * C v u * (x 0 v * y 0 u).
Used by 1 declaration in 1 file
lemma mxtrace_sandwich_le main result source, line 123 
forall {R : realType} {n : nat} [K A : 'M_n] [a b : nat],
K \is symmetricmx ->
A \is symmetricmx ->
~~ odd (a + b) -> `|\tr (K *m A ^+ a *m K *m A ^+ b)| <= \tr (K ^+ 2 *m A ^+ (a + b))

|tr (K A^a K A^b)| <= tr (K^2 A^(a+b)) for K, A symmetric and a + b even. In an eigenbasis of A, with C = P K P^T, the left side is at most \sum_(u, v) C_uv^2 |d_v|^a |d_u|^b, which exprn_cross_le and the symmetry of C bound by \sum_(u, v) C_uv^2 |d_u|^(a+b).

Main result, as the README states it

|tr (K A^a K A^b)| <= tr (K^2 A^(a+b)) for symmetric K and A and a + b even. tr (S T) <= opnorm S tr T for T positive semidefinite (psdmx T) and any square S. For a probability P, a measurable f >= 0 and k >= 0, E f <= (E f^(k+1))^(1/(k+1)), the expectations being integrals in the extended reals, and E f^(k+1) <= t^(k+1) with t > 0 gives E f <= t.

Statement as written in the source
Lemma mxtrace_sandwich_le (K A : 'M[R]_n) a b :
  K \is symmetricmx -> A \is symmetricmx -> ~~ odd (a + b) ->
  `|\tr (K *m A ^+ a *m K *m A ^+ b)| <= \tr (K ^+ 2 *m A ^+ (a + b)).
Used by 1 declaration in 1 file
lemma mxtrace_mul_psd_le main result source, line 180 
forall {R : realType} {n : nat} (S : 'M_n) [T : 'M_n],
psdmx T -> \tr (S *m T) <= opnorm S * \tr T

tr (S T) <= opnorm S tr T for T positive semidefinite: in an eigenbasis of T, the diagonal entries of S are at most opnorm S.

Main result

Stated in the README together with mxtrace_sandwich_le.

Statement as written in the source
Lemma mxtrace_mul_psd_le (S T : 'M[R]_n) : psdmx T ->
  \tr (S *m T) <= opnorm S * \tr T.
Used by 1 declaration in 1 file
lemma psdmx_exp_even source, line 198 
forall {R : realType} {n : nat} [A : 'M_n] (k : nat),
A \is symmetricmx -> psdmx (A ^+ k.*2)
Statement as written in the source
Lemma psdmx_exp_even (A : 'M[R]_n) k : A \is symmetricmx -> psdmx (A ^+ k.*2).
Used by 1 declaration in 1 file
sectionmoment_root
Context d (T : measurableType d) (R : realType) (P : probability T R).
lemma young_exprn source, line 212 
forall [R : realType] [x t : R] (p : nat),
0 <= x -> 0 <= t -> p.+1%:R * x * t ^+ p <= p%:R * t ^+ p.+1 + x ^+ p.+1

Young's inequality with integer exponents: (p + 1) x t^p <= p t^(p+1) + x^(p+1) for x, t >= 0.

Statement as written in the source
Lemma young_exprn (x t : R) p : 0 <= x -> 0 <= t ->
  p.+1%:R * x * t ^+ p <= p%:R * t ^+ p.+1 + x ^+ p.+1.
Used by 1 declaration in 1 file
lemma moment_root_le main result source, line 230 
forall [d : measure_display] [T : measurableType d] [R : realType] 
  [P : probability T R] [f : T -> R] [k : nat] [t : R],
measurable_fun [set: T] f ->
(forall x : T, 0 <= f x) ->
0 < t -> (\int[P]_x (f x ^+ k.+1)%:E <= (t ^+ k.+1)%:E)%E -> (\int[P]_x (f x)%:E <= t%:E)%E

The moment inequality E f <= (E f^(k+1))^(1/(k+1)) for f >= 0, in the form: E f^(k+1) <= t^(k+1) with t > 0 gives E f <= t. Integrate Young's inequality (k + 1) t^k f <= k t^(k+1) + f^(k+1).

Main result

Stated in the README together with mxtrace_sandwich_le.

Statement as written in the source
Lemma moment_root_le (f : T -> R) k (t : R) : measurable_fun [set: T] f ->
  (forall x, 0 <= f x) -> 0 < t ->
  (\int[P]_x (f x ^+ k.+1)%:E <= (t ^+ k.+1)%:E)%E ->
  (\int[P]_x (f x)%:E <= t%:E)%E.
Used by 2 declarations in 1 file
lemma moment_root_powR main result source, line 268 
forall [d : measure_display] [T : measurableType d] [R : realType] 
  [P : probability T R] [f : T -> R] [k : nat] [M : R],
measurable_fun [set: T] f ->
(forall x : T, 0 <= f x) ->
(\int[P]_x (f x ^+ k.+1)%:E <= M%:E)%E -> (\int[P]_x (f x)%:E <= (M `^ k.+1%:R^-1)%:E)%E

The same with a bound M of E f^(k+1): E f <= M^(1/(k+1)).

Main result

Stated in the README together with mxtrace_sandwich_le.

Statement as written in the source
Lemma moment_root_powR (f : T -> R) k (M : R) : measurable_fun [set: T] f ->
  (forall x, 0 <= f x) ->
  (\int[P]_x (f x ^+ k.+1)%:E <= M%:E)%E ->
  (\int[P]_x (f x)%:E <= (M `^ k.+1%:R^-1)%:E)%E.
Used by 1 declaration in 1 file
sectiongauss_mx_series
Context {R : realType} {n r : nat}.
Local Notation gauss := (@gauss R).
Variable H : 'I_r -> 'M[R]_n.
lemma series_sym source, line 294 
forall {R : realType} {n r : nat} [H : 'I_r -> 'M_n] (g : 'rV_r),
(forall j : 'I_r, H j \is symmetricmx) -> \sum_j g 0 j *: H j \is symmetricmx
Statement as written in the source
Lemma series_sym (g : 'rV[R]_r) : (forall j, H j \is symmetricmx) ->
  \sum_j g 0 j *: H j \is symmetricmx.
Used by 1 declaration in 1 file
lemma mx_polyfun_series source, line 301 
forall {R : realType} {n r : nat} (H : 'I_r -> 'M_n),
mx_polyfun (fun g : 'rV_r => \sum_j g 0 j *: H j)
Statement as written in the source
Lemma mx_polyfun_series : mx_polyfun (fun g : 'rV[R]_r => \sum_j g 0 j *: H j).
Used by 5 declarations in 1 file
lemma series_lin source, line 308 
forall {R : realType} {n r : nat} (H : 'I_r -> 'M_n) (h : R) (x v : 'rV_r),
\sum_j (h *: v + x) 0 j *: H j = h *: \sum_j v 0 j *: H j + \sum_j x 0 j *: H j
Statement as written in the source
Lemma series_lin (h : R) (x v : 'rV[R]_r) :
  \sum_j (h *: v + x) 0 j *: H j =
  h *: (\sum_j v 0 j *: H j) + \sum_j x 0 j *: H j.
Used by 1 declaration in 1 file
lemma series_delta source, line 316 
forall {R : realType} {n r : nat} (H : 'I_r -> 'M_n) (j : 'I_r),
\sum_l ('e_j : 'rV_r) 0 l *: H l = H j
Statement as written in the source
Lemma series_delta (j : 'I_r) :
  \sum_l (delta_mx 0 j : 'rV[R]_r) 0 l *: H l = H j.
Used by 1 declaration in 1 file
lemma is_derive_series_pow source, line 324 
forall {R : realType} {n r : nat} (H : 'I_r -> 'M_n) (k : nat) (u v : 'I_n) (x w : 'rV_r),
is_derive x w (fun g : 'rV_r => ((\sum_l g 0 l *: H l) ^+ k) u v)
  (mxpow_deriv (\sum_l x 0 l *: H l) (\sum_l w 0 l *: H l) k u v)
Statement as written in the source
Lemma is_derive_series_pow k (u v : 'I_n) (x w : 'rV[R]_r) :
  is_derive x w (fun g : 'rV[R]_r => ((\sum_l g 0 l *: H l) ^+ k) u v)
    (mxpow_deriv (\sum_l x 0 l *: H l) (\sum_l w 0 l *: H l) k u v).
Used by 1 declaration in 1 file
lemma gauss_mx_series_ibp_coord source, line 337 
forall {R : realType} {n r : nat} (H : 'I_r -> 'M_n) (k : nat) (j : 'I_r) (A : 'M_n),
\int[gauss r]_g (g 0 j * \tr (A *m (\sum_l g 0 l *: H l) ^+ k)) =
\int[gauss r]_g \tr (A *m mxpow_deriv (\sum_l g 0 l *: H l) (H j) k)

Gaussian integration by parts in the coordinate g_j: E[g_j tr (A X^k)] = E[tr (A D_j)], where D_j is the derivative of X^k along H_j.

Statement as written in the source
Lemma gauss_mx_series_ibp_coord k (j : 'I_r) (A : 'M[R]_n) :
  \int[gauss r]_g (g 0 j * \tr (A *m (\sum_l g 0 l *: H l) ^+ k)) =
  \int[gauss r]_g \tr (A *m mxpow_deriv (\sum_l g 0 l *: H l) (H j) k).
Used by 1 declaration in 1 file
lemma gauss_mx_series_ibp main result source, line 375 
forall {R : realType} {n r : nat} (H : 'I_r -> 'M_n) (k : nat),
\int[gauss r]_g \tr ((\sum_j g 0 j *: H j) ^+ k.+1) =
\sum_j \int[gauss r]_g \tr (H j *m mxpow_deriv (\sum_l g 0 l *: H l) (H j) k)

E tr X^(k+1) = \sum_j E tr (H_j D_j), with D_j the derivative of X^k along H_j: Gaussian integration by parts in every coordinate.

Main result

Stated in the README together with gauss_mx_series_moment.

Statement as written in the source
Lemma gauss_mx_series_ibp k :
  \int[gauss r]_g \tr ((\sum_j g 0 j *: H j) ^+ k.+1) =
  \sum_j \int[gauss r]_g \tr (H j *m mxpow_deriv (\sum_l g 0 l *: H l) (H j) k).
Used by 2 declarations in 1 file
lemma gauss_mx_series_trace_sqr main result source, line 393 
forall {R : realType} {n r : nat} (H : 'I_r -> 'M_n),
\int[gauss r]_g \tr ((\sum_j g 0 j *: H j) ^+ 2) = \tr (\sum_j H j ^+ 2)

E tr X^2 = tr S.

Main result

Stated in the README together with gauss_mx_series_moment.

Statement as written in the source
Lemma gauss_mx_series_trace_sqr :
  \int[gauss r]_g \tr ((\sum_j g 0 j *: H j) ^+ 2) = \tr (\sum_j H j ^+ 2).
Used by 1 declaration in 1 file
theorem gauss_mx_series_trace_rec main result source, line 403 
forall {R : realType} {n r : nat} [H : 'I_r -> 'M_n] (q : nat),
(forall j : 'I_r, H j \is symmetricmx) ->
\int[gauss r]_g \tr ((\sum_j g 0 j *: H j) ^+ q.+1.*2) <=
q.*2.+1%:R * opnorm (\sum_j H j ^+ 2) * \int[gauss r]_g \tr ((\sum_j g 0 j *: H j) ^+ q.*2)

The recursion E tr X^(2q+2) <= (2q+1) opnorm S E tr X^(2q).

Main result

Stated in the README together with gauss_mx_series_moment.

Statement as written in the source
Theorem gauss_mx_series_trace_rec q : (forall j, H j \is symmetricmx) ->
  \int[gauss r]_g \tr ((\sum_j g 0 j *: H j) ^+ q.+1.*2) <=
  q.*2.+1%:R * opnorm (\sum_j H j ^+ 2) *
    \int[gauss r]_g \tr ((\sum_j g 0 j *: H j) ^+ q.*2).
Used by 1 declaration in 1 file
lemma gauss_mx_series_trace_le source, line 438 
forall {R : realType} {n r : nat} [H : 'I_r -> 'M_n] [q : nat],
(forall j : 'I_r, H j \is symmetricmx) ->
(0 < q)%N ->
\int[gauss r]_g \tr ((\sum_j g 0 j *: H j) ^+ q.*2) <=
\prod_(i < q) i.*2.+1%:R * opnorm (\sum_j H j ^+ 2) ^+ q.-1 * \tr (\sum_j H j ^+ 2)
Statement as written in the source
Lemma gauss_mx_series_trace_le q : (forall j, H j \is symmetricmx) ->
  (0 < q)%N ->
  \int[gauss r]_g \tr ((\sum_j g 0 j *: H j) ^+ q.*2) <=
  (\prod_(i < q) i.*2.+1%:R) * opnorm (\sum_j H j ^+ 2) ^+ q.-1 *
    \tr (\sum_j H j ^+ 2).
Used by 1 declaration in 1 file
theorem gauss_mx_series_moment main result source, line 458 
forall {R : realType} {n r : nat} [H : 'I_r -> 'M_n] [q : nat],
(forall j : 'I_r, H j \is symmetricmx) ->
(0 < q)%N ->
(\int[gauss r]_g (\tr ((\sum_j g 0 j *: H j) ^+ q.*2))%:E <=
 (\prod_(i < q) i.*2.+1%:R * opnorm (\sum_j H j ^+ 2) ^+ q.-1 * \tr (\sum_j H j ^+ 2))%:E)%E

The moment bound E tr X^(2q) <= (2q - 1)!! opnorm S^(q-1) tr S, as an integral of a nonnegative function in the extended reals.

Main result, as the README states it

Gaussian matrix series. For symmetric H_1, ..., H_r in 'M[R]_n, S = \sum_j H_j^2 and g of law gauss r, the series X = \sum_j g_j H_j satisfies E tr X^(2q) <= (2q - 1)!! opnorm S^(q-1) tr S for every q >= 1, with no dimension in the bound (an integral in the extended reals). It follows from E tr X^2 = tr S, which needs no symmetry, and the recursion E tr X^(2q+2) <= (2q + 1) opnorm S E tr X^(2q). The recursion comes from Gaussian integration by parts in each coordinate, E tr X^(k+1) = \sum_j E tr (H_j D_j) with D_j the derivative of X^k along H_j. Lemma 4.2 of the fourfold ergodic paper of family 154 of the OpenAI math collection (revision 1581d4cbd).

Statement as written in the source
Theorem gauss_mx_series_moment q : (forall j, H j \is symmetricmx) ->
  (0 < q)%N ->
  (\int[gauss r]_g (\tr ((\sum_j g 0 j *: H j) ^+ q.*2))%:E <=
   ((\prod_(i < q) i.*2.+1%:R) * opnorm (\sum_j H j ^+ 2) ^+ q.-1 *
     \tr (\sum_j H j ^+ 2))%:E)%E.
Used by 2 declarations in 2 files
sectionsym_dilation
Context {R : realType}.
definition sym_dilation source, line 477
Type
forall {R : realType} [m p : nat], 'M_(m, p) -> 'M_(m + p)
Definition
Definition sym_dilation m p (B : 'M[R]_(m, p)) : 'M[R]_(m + p) :=
  block_mx 0 B B^T 0.

The symmetric dilation [[0, B], [B^T, 0]] of a rectangular matrix.

Used by 5 declarations in 1 file
lemma sym_dilation_sym source, line 480 
forall {R : realType} [m p : nat] (B : 'M_(m, p)), sym_dilation B \is symmetricmx
Statement as written in the source
Lemma sym_dilation_sym m p (B : 'M[R]_(m, p)) : sym_dilation B \is symmetricmx.
Used by 1 declaration in 1 file
lemma sym_dilation_series source, line 485 
forall {R : realType} [m p r : nat] (g : 'rV_r) (B : 'I_r -> 'M_(m, p)),
sym_dilation (\sum_j g 0 j *: B j) = \sum_j g 0 j *: sym_dilation (B j)
Statement as written in the source
Lemma sym_dilation_series m p r (g : 'rV[R]_r) (B : 'I_r -> 'M[R]_(m, p)) :
  sym_dilation (\sum_j g 0 j *: B j) = \sum_j g 0 j *: sym_dilation (B j).
Used by 1 declaration in 1 file
lemma sym_dilation_sqr source, line 497 
forall {R : realType} [m p : nat] (B : 'M_(m, p)),
sym_dilation B ^+ 2 = block_mx (B *m B^T) 0 0 (B^T *m B)
Statement as written in the source
Lemma sym_dilation_sqr m p (B : 'M[R]_(m, p)) :
  sym_dilation B ^+ 2 = block_mx (B *m B^T) 0 0 (B^T *m B).
Used by 1 declaration in 1 file
lemma mxdot_col_mx source, line 504 
forall {R : realType} [m1 m2 n : nat] (A C : 'M_(m1, n)) (B D : 'M_(m2, n)),
mxdot (col_mx A B) (col_mx C D) = mxdot A C + mxdot B D
Statement as written in the source
Lemma mxdot_col_mx m1 m2 n (A C : 'M[R]_(m1, n)) (B D : 'M[R]_(m2, n)) :
  mxdot (col_mx A B) (col_mx C D) = mxdot A C + mxdot B D.
Used by 2 declarations in 1 file
lemma mxdot_mulmx_opnorm_le source, line 511 
forall {R : realType} [m n : nat] [N : 'M_(m, n)] (y : 'cV_n) [b : R],
opnorm N <= b -> mxdot (N *m y) (N *m y) <= b ^+ 2 * mxdot y y
Statement as written in the source
Lemma mxdot_mulmx_opnorm_le m n (N : 'M[R]_(m, n)) (y : 'cV[R]_n) (b : R) :
  opnorm N <= b -> mxdot (N *m y) (N *m y) <= b ^+ 2 * mxdot y y.
Used by 1 declaration in 1 file
lemma opnorm_block_diag_le source, line 520 
forall {R : realType} [m1 n1 m2 n2 : nat] (A : 'M_(m1, n1)) (D : 'M_(m2, n2)),
opnorm (block_mx A 0 0 D) <= maxr (opnorm A) (opnorm D)
Statement as written in the source
Lemma opnorm_block_diag_le m1 n1 m2 n2 (A : 'M[R]_(m1, n1))
    (D : 'M[R]_(m2, n2)) :
  opnorm (block_mx A 0 0 D) <= Num.max (opnorm A) (opnorm D).
Used by 1 declaration in 1 file
lemma opnorm_le_sym_dilation source, line 533 
forall {R : realType} [m p : nat] (B : 'M_(m, p)), opnorm B <= opnorm (sym_dilation B)
Statement as written in the source
Lemma opnorm_le_sym_dilation m p (B : 'M[R]_(m, p)) :
  opnorm B <= opnorm (sym_dilation B).
Used by 1 declaration in 1 file
sectionseries_log_bound
Context {R : realType}.
lemma expR1_le4 source, line 550 
forall {R : realType}, (expR 1 : R) <= (4 : R)
Statement as written in the source
Lemma expR1_le4 : expR 1 <= 4 :> R.
Used by 2 declarations in 2 files
lemma ln2D_ge source, line 563 
forall {R : realType} [d : R], 1 <= d -> 2 / 3 <= ln (2 + d)

ln x >= 1 - 1 / x, at x = 2 + d >= 3.

Statement as written in the source
Lemma ln2D_ge (d : R) : 1 <= d -> 2 / 3 <= ln (2 + d).
Used by 4 declarations in 2 files
lemma series_log_bound source, line 574 
forall {R : realType} [d s2 tau : R],
1 <= d ->
0 <= s2 ->
s2 <= Num.ExtraDef.sqrtr d ->
0 <= tau ->
tau <= 2 * d ->
\prod_(i < (truncn (ln (2 + d))).+1) i.*2.+1%:R * s2 ^+ truncn (ln (2 + d)) * tau <=
(5 * d `^ 4^-1 * Num.ExtraDef.sqrtr (ln (2 + d))) ^+ (truncn (ln (2 + d))).+1.*2

The arithmetic of the choice q = floor (ln (2 + d)) + 1: if s2 <= sqrt d and tau <= 2 d with d >= 1, then (2q - 1)!! s2^(q-1) tau <= (5 d^(1/4) sqrt (ln (2 + d)))^(2q).

Statement as written in the source
Lemma series_log_bound (d s2 tau : R) : 1 <= d -> 0 <= s2 ->
  s2 <= Num.sqrt d -> 0 <= tau -> tau <= 2 * d ->
  (\prod_(i < (truncn (ln (2 + d))).+1) i.*2.+1%:R) *
    s2 ^+ truncn (ln (2 + d)) * tau <=
  (5 * d `^ 4^-1 * Num.sqrt (ln (2 + d))) ^+ (truncn (ln (2 + d))).+1.*2.
Used by 1 declaration in 1 file
sectiongauss_mx_series_rect
Context {R : realType} {m p r : nat}.
Local Notation gauss := (@gauss R).
Variable B : 'I_r -> 'M[R]_(m, p).
lemma series_opnorm_lipschitz source, line 636 
forall {R : realType} {m p r : nat} (B : 'I_r -> 'M_(m, p)) (g h : 'rV_r),
`|opnorm (\sum_j g 0 j *: B j) - opnorm (\sum_j h 0 j *: B j)| <=
(\sum_j frobenius (B j)) * frobenius (g - h)
Statement as written in the source
Lemma series_opnorm_lipschitz (g h : 'rV[R]_r) :
  `|opnorm (\sum_j g 0 j *: B j) - opnorm (\sum_j h 0 j *: B j)| <=
  (\sum_j frobenius (B j)) * frobenius (g - h).
Used by 3 declarations in 2 files
lemma measurable_series_opnorm source, line 649 
forall {R : realType} {m p r : nat} (B : 'I_r -> 'M_(m, p)),
measurable_fun [set: 'rV_r]
  (fun g : 'rV_r =>
   opnorm (\sum_j g 0 j *: B j))
Statement as written in the source
Lemma measurable_series_opnorm :
  measurable_fun [set: 'rV[R]_r] (fun g => opnorm (\sum_j g 0 j *: B j)).
Used by 3 declarations in 1 file
theorem gauss_mx_series_opnorm_moment main result source, line 659 
forall {R : realType} {m p r : nat} (B : 'I_r -> 'M_(m, p)) [q : nat],
(0 < q)%N ->
(\int[gauss r]_g (opnorm (\sum_j g 0 j *: B j) ^+ q.*2)%:E <=
 (\prod_(i < q) i.*2.+1%:R *
  maxr (opnorm (\sum_j B j *m (B j)^T)) (opnorm (\sum_j (B j)^T *m B j)) ^+ q.-1 *
  (2 * \tr (\sum_j B j *m (B j)^T)))%:E)%E

E opnorm (\sum_j g_j B_j)^(2q) <= (2q - 1)!! sigma^(2(q-1)) tau, with sigma^2 = max (opnorm (\sum_j B_j B_j^T)) (opnorm (\sum_j B_j^T B_j)) and tau = 2 tr (\sum_j B_j B_j^T), through the symmetric dilation.

Main result

Stated in the README together with gauss_mx_series_opnorm.

Statement as written in the source
Theorem gauss_mx_series_opnorm_moment q : (0 < q)%N ->
  (\int[gauss r]_g (opnorm (\sum_j g 0 j *: B j) ^+ q.*2)%:E <=
   ((\prod_(i < q) i.*2.+1%:R) *
     Num.max (opnorm (\sum_j B j *m (B j)^T)) (opnorm (\sum_j (B j)^T *m B j))
       ^+ q.-1 * (2 * \tr (\sum_j B j *m (B j)^T)))%:E)%E.
Used by 2 declarations in 1 file
theorem gauss_mx_series_opnorm main result source, line 702 
forall {R : realType} {m p r : nat} (B : 'I_r -> 'M_(m, p)) [q : nat],
(0 < q)%N ->
(\int[gauss r]_g (opnorm (\sum_j g 0 j *: B j))%:E <=
 ((\prod_(i < q) i.*2.+1%:R *
   maxr (opnorm (\sum_j B j *m (B j)^T)) (opnorm (\sum_j (B j)^T *m B j)) ^+ q.-1 *
   (2 * \tr (\sum_j B j *m (B j)^T)))
  `^ q.*2%:R^-1)%:E)%E

The rectangular bound: E opnorm (\sum_j g_j B_j) <= ((2q - 1)!! sigma^(2(q-1)) tau)^(1/(2q)) for every q >= 1. No dimension of the matrices appears.

Main result, as the README states it

For B_1, ..., B_r in 'M[R]_(m, p) and g of law gauss r, with sigma^2 = max (opnorm (\sum_j B_j B_j^T), opnorm (\sum_j B_j^T B_j)) and tau = 2 tr (\sum_j B_j B_j^T): E opnorm (\sum_j g_j B_j)^(2q) <= (2q - 1)!! sigma^(2(q-1)) tau and E opnorm (\sum_j g_j B_j) <= ((2q - 1)!! sigma^(2(q-1)) tau)^(1/(2q)) for every q >= 1, through the symmetric dilation sym_dilation B_j = [[0, B_j], [B_j^T, 0]]. If the two operator norms are at most sqrt d and tr (\sum_j B_j B_j^T) <= d for a real d >= 1, then E opnorm (\sum_j g_j B_j) <= 5 d^(1/4) sqrt (ln (2 + d)). No dimension of the matrices enters.

Statement as written in the source
Theorem gauss_mx_series_opnorm q : (0 < q)%N ->
  (\int[gauss r]_g (opnorm (\sum_j g 0 j *: B j))%:E <=
   (((\prod_(i < q) i.*2.+1%:R) *
     Num.max (opnorm (\sum_j B j *m (B j)^T)) (opnorm (\sum_j (B j)^T *m B j))
       ^+ q.-1 * (2 * \tr (\sum_j B j *m (B j)^T))) `^ (q.*2%:R)^-1)%:E)%E.
Used by 1 declaration in 1 file
theorem gauss_mx_series_opnorm_log main result source, line 720 
forall {R : realType} {m p r : nat} [B : 'I_r -> 'M_(m, p)] [d : R],
1 <= d ->
opnorm (\sum_j B j *m (B j)^T) <= Num.ExtraDef.sqrtr d ->
opnorm (\sum_j (B j)^T *m B j) <= Num.ExtraDef.sqrtr d ->
\tr (\sum_j B j *m (B j)^T) <= d ->
(\int[gauss r]_g (opnorm (\sum_j g 0 j *: B j))%:E <=
 (5 * d `^ 4^-1 * Num.ExtraDef.sqrtr (ln (2 + d)))%:E)%E

The form of Lemma 4.2 of the fourfold paper of family 154, with C = 5: E opnorm (\sum_j g_j B_j) <= 5 d^(1/4) sqrt (ln (2 + d)) when the diagonal blocks \sum_j B_j B_j^T and \sum_j B_j^T B_j of the dilation S have operator norms at most sqrt d and tr (\sum_j B_j B_j^T) <= d, that is opnorm S <= sqrt d and tr S <= 2 d, for a real d >= 1. The proof takes q = floor (ln (2 + d)) + 1 in gauss_mx_series_opnorm_moment.

Main result

Stated in the README together with gauss_mx_series_opnorm.

Statement as written in the source
Theorem gauss_mx_series_opnorm_log (d : R) : 1 <= d ->
  opnorm (\sum_j B j *m (B j)^T) <= Num.sqrt d ->
  opnorm (\sum_j (B j)^T *m B j) <= Num.sqrt d ->
  \tr (\sum_j B j *m (B j)^T) <= d ->
  (\int[gauss r]_g (opnorm (\sum_j g 0 j *: B j))%:E <=
   (5 * d `^ 4^-1 * Num.sqrt (ln (2 + d)))%:E)%E.
Used by 2 declarations in 2 files
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.