OAI/Probability/SKGap/Matrix/MatrixWordRegularity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.matrixFactorProduct line 14
2. lemma OAI.SKGap.matrixFactorProduct_nil line 18
3. lemma OAI.SKGap.matrixFactorProduct_cons line 20
4. lemma OAI.SKGap.matrixFactorProduct_opNorm line 24
5. theorem OAI.SKGap.matrixFactorProduct_lipschitz line 34
6. lemma OAI.SKGap.matrixFactorProduct_entry_lipschitz line 64
7. lemma OAI.SKGap.matrixFactorProduct_trace_lipschitz line 69
8. lemma OAI.SKGap.goe_word_entry_lipschitz line 83
9. lemma OAI.SKGap.goe_word_normalized_trace_lipschitz line 90