OAI/Analysis/FreeWords/MatrixL2Closure.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.KKMatrixL2.traceNorm_sum_leline 27 - theorem
OAI.KKMatrixL2.matrix_l2_asymp_mulline 32
OAI/Analysis/FreeWords/MatrixL2Closure.lean2 declarations, 0 contain sorry, 0 declared as axioms
OAI.KKMatrixL2.traceNorm_sum_le line 27OAI.KKMatrixL2.matrix_l2_asymp_mul line 32