OAI/Probability/SKGap/Matrix/StartedWordClosure.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.Recipe.ClosedWordDiagramBound line 18
2. def OAI.SKGapCutoff.Recipe.initialTraceBudget line 22
3. lemma OAI.SKGapCutoff.Recipe.initialTraceBudget_nonneg line 23
4. theorem OAI.SKGapCutoff.Recipe.OrdinaryData.implicit_started_word_closure line 31
5. lemma OAI.SKGapCutoff.Recipe.closedWordBounded_iff line 112
6. def OAI.SKGapCutoff.Recipe.ClosedWordSeminormBound line 116
7. lemma OAI.SKGapCutoff.Recipe.ClosedWordSeminormBound.mono line 121
8. lemma OAI.SKGapCutoff.Recipe.ClosedWordSeminormBound.diagram line 125
9. def OAI.SKGapCutoff.Recipe.ClosedWordEvent line 128
10. theorem OAI.SKGapCutoff.Recipe.closed_word_event line 133
11. theorem OAI.SKGapCutoff.Recipe.closed_word_test_budget line 150