OAI/Analysis/FreeWords/MatrixEnergyDecrease.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KKMatrixQuantization.unitary_norm_le_one line 21
2. theorem OAI.KKMatrixQuantization.algebraConj_traceNorm_sub_le line 31
3. theorem OAI.KKMatrixQuantization.finite_polynomial_slack line 59
4. theorem OAI.KKMatrixQuantization.exists_matrix_energy_decrease line 71