OAI/Probability/SKGap/Matrix/ClosedErrorTrace.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SKGapCutoff.Recipe.finite_graph_trace_tested line 15
2. def OAI.SKGapCutoff.Recipe.closedWordBounded line 85
3. def OAI.SKGapCutoff.Recipe.ClosedWordTestBound line 88
4. lemma OAI.SKGapCutoff.Recipe.closedWordBounded_append line 93
5. lemma OAI.SKGapCutoff.Recipe.closedWordBounded_lift line 98
6. lemma OAI.SKGapCutoff.Recipe.implicit_error_elimination line 106
7. theorem OAI.SKGapCutoff.Recipe.implicit_trace_bound line 119
8. theorem OAI.SKGapCutoff.Recipe.implicit_source_field_trace line 149
9. lemma OAI.SKGapCutoff.Recipe.ClosedWordTestBound.ordinary line 176
10. theorem OAI.SKGapCutoff.Recipe.closed_finite_graph_trace line 183