OAI/Probability/SKGap/Matrix/BufferedClosedWord.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.Recipe.inverseDenominator line 15
2. lemma OAI.SKGapCutoff.Recipe.continuous_inverseDenominator line 18
3. lemma OAI.SKGapCutoff.Recipe.continuousAt_exactWord line 23
4. lemma OAI.SKGapCutoff.Recipe.continuous_stability_lower line 45
5. def OAI.SKGapCutoff.Recipe.BufferedClosedWordEvent line 52
6. lemma OAI.SKGapCutoff.Recipe.isClosed_bufferedClosedWordEvent line 57
7. lemma OAI.SKGapCutoff.Recipe.ClosedWordEvent.buffered line 75
8. theorem OAI.SKGapCutoff.Recipe.disorder_buffered_closed_word_event line 80
9. lemma OAI.SKGapCutoff.Recipe.inverseDenominator_det_ne line 92
10. lemma OAI.SKGapCutoff.Recipe.BufferedClosedWordEvent.unbuffer line 114
11. theorem OAI.SKGapCutoff.Recipe.disorder_closed_word_event line 121
12. theorem OAI.SKGapCutoff.Recipe.disorder_started_matrix_event line 144