OAI/Probability/SKGap/Matrix/MatrixEntryCLM.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.matrix_entry_le_frobenius line 21
2. def OAI.SKGap.matrixEntryCLM line 29
3. lemma OAI.SKGap.matrixEntry_lipschitz line 35
4. lemma OAI.SKGap.matrixEntry_derivative line 42
5. lemma OAI.SKGap.matrix_inverse_diff_bound line 47
6. def OAI.SKGap.diagonalVector line 57
7. lemma OAI.SKGap.diagonalVector_norm_le line 60
8. lemma OAI.SKGap.abs_trace_le_frobenius line 69
9. lemma OAI.SKGap.matrixTrace_mul_lipschitz line 80