OAI/Probability/SKGap/Localization/MarkedDiagnostic.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Recipe.wordBounded_append line 14
2. lemma OAI.SKGapCutoff.Recipe.wordBounded_mono line 20
3. def OAI.SKGapCutoff.Recipe.MarkControl line 26
4. def OAI.SKGapCutoff.Recipe.MarkedControl line 29
5. def OAI.SKGapCutoff.Recipe.PairControl line 31
6. lemma OAI.SKGapCutoff.Recipe.MarkControl.mono line 33
7. lemma OAI.SKGapCutoff.Recipe.MarkControl.prepend line 36
8. lemma OAI.SKGapCutoff.Recipe.MarkedControl.append line 56
9. lemma OAI.SKGapCutoff.Recipe.MarkedControl.mono line 62
10. lemma OAI.SKGapCutoff.Recipe.MarkedControl.prepend line 65
11. lemma OAI.SKGapCutoff.Recipe.MarkedControl.scale line 72
12. lemma OAI.SKGapCutoff.Recipe.diagonalWords_control line 78
13. lemma OAI.SKGapCutoff.Recipe.averageWords_control line 87
14. lemma OAI.SKGapCutoff.Recipe.zeroPair_control line 95
15. lemma OAI.SKGapCutoff.Recipe.smallBranch_control line 108
16. lemma OAI.SKGapCutoff.Recipe.boundedBranch_control line 119