On this page
Gaussian matrix series: the theorem
Imports 4 library modules and 16 external
- GaussianAnalysis.gaussian.gauss
- GaussianAnalysis.matrix.opnorm
- GaussianAnalysis.random_matrix.matrix_series
- GaussianApplications.MatrixSeriesStatement
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.classical.boolp, mathcomp.classical.classical_sets, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.analysis.exp, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.probability_theory.probability, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.field_tactic
Target T1 of phase 12. matrix_series_theorem proves matrix_series_statement of MatrixSeriesStatement.v from the library file random_matrix/matrix_series.v, which 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' (family 154 of the OpenAI math collection, revision 1581d4cbd, sections/04-packing.tex). The collection has no Lean version of it.
- (a) is gauss_mx_series_moment, with H_j H_j = H_j^2.
- (b) is gauss_mx_series_opnorm.
- (c) is gauss_mx_series_opnorm_log with C = 5: the hypothesis on the maximum of the two operator norms gives each of them, 2 tr (\sum_j B_j B_j^T) <= 2 d gives tr (\sum_j B_j B_j^T) <= d, and sqrt (sqrt d) = d^(1/4).
Main results
| Results | Statement |
|---|---|
Proves matrix_series_statement (T1). (a) For symmetric H_1, ..., H_r in 'M[R]_n, S = \sum_j H_j H_j and g of law gauss r, E tr (\sum_j g_j H_j)^(2q) <= (2q - 1)!! opnorm S^(q-1) tr S for every q >= 1 (gauss_mx_series_moment). (b) For B_1, ..., B_r in 'M[R]_(m, p) and every q >= 1, E opnorm (\sum_j g_j B_j) <= ((2q - 1)!! sigma^(2(q-1)) tau)^(1/(2q)), 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) (gauss_mx_series_opnorm). (c) With C = 5: if sigma^2 <= sqrt d and tau <= 2 d for a real d >= 1, then E opnorm (\sum_j g_j B_j) <= 5 sqrt (sqrt d) sqrt (ln (2 + d)) (gauss_mx_series_opnorm_log). The expectations are integrals in the extended reals. Axioms: three of boolp. |
Declarations1 exported
Proves matrix_series_statement (T1). (a) For symmetric H_1, ..., H_r in 'M[R]_n, S = \sum_j H_j H_j and g of law gauss r, E tr (\sum_j g_j H_j)^(2q) <= (2q - 1)!! opnorm S^(q-1) tr S for every q >= 1 (gauss_mx_series_moment). (b) For B_1, ..., B_r in 'M[R]_(m, p) and every q >= 1, E opnorm (\sum_j g_j B_j) <= ((2q - 1)!! sigma^(2(q-1)) tau)^(1/(2q)), 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) (gauss_mx_series_opnorm). (c) With C = 5: if sigma^2 <= sqrt d and tau <= 2 d for a real d >= 1, then E opnorm (\sum_j g_j B_j) <= 5 sqrt (sqrt d) sqrt (ln (2 + d)) (gauss_mx_series_opnorm_log). The expectations are integrals in the extended reals. Axioms: three of boolp.
Statement as written in the source
Theorem matrix_series_theorem : matrix_series_statement.