OAI/Probability/SKGap/Localization/ClosedMarkedControl.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.Noncrossing.ClosedMarked.closedWordBounded_diag line 15
2. def OAI.SKGap.Noncrossing.ClosedMarked.MarkControl line 20
3. def OAI.SKGap.Noncrossing.ClosedMarked.MarkedControl line 23
4. def OAI.SKGap.Noncrossing.ClosedMarked.PairControl line 25
5. lemma OAI.SKGap.Noncrossing.ClosedMarked.MarkControl.mono line 27
6. lemma OAI.SKGap.Noncrossing.ClosedMarked.MarkControl.prepend line 30
7. lemma OAI.SKGap.Noncrossing.ClosedMarked.MarkedControl.append line 50
8. lemma OAI.SKGap.Noncrossing.ClosedMarked.MarkedControl.mono line 56
9. lemma OAI.SKGap.Noncrossing.ClosedMarked.MarkedControl.prepend line 59
10. lemma OAI.SKGap.Noncrossing.ClosedMarked.MarkedControl.scale line 66
11. lemma OAI.SKGap.Noncrossing.ClosedMarked.diagonalWords_control line 72
12. lemma OAI.SKGap.Noncrossing.ClosedMarked.averageWords_control line 81
13. lemma OAI.SKGap.Noncrossing.ClosedMarked.zeroPair_control line 89
14. lemma OAI.SKGap.Noncrossing.ClosedMarked.smallBranch_control line 102
15. lemma OAI.SKGap.Noncrossing.ClosedMarked.boundedBranch_control line 113
16. def OAI.SKGap.Noncrossing.ClosedMarked.GradedControl line 139
17. lemma OAI.SKGap.Noncrossing.ClosedMarked.PairControl.mono line 142
18. lemma OAI.SKGap.Noncrossing.ClosedMarked.implicitPair_control line 144
19. lemma OAI.SKGap.Noncrossing.ClosedMarked.SmallTree.smallBranches_control line 168
20. lemma OAI.SKGap.Noncrossing.ClosedMarked.SmallTree.boundedBranches_control line 178
21. theorem OAI.SKGapCutoff.Recipe.OrdinaryData.startedMarked_control line 197