OAI/Combinatorics/RamseyFive/Iteration/WindowStage.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SharpRamseyFive.SelectedTuple.windowFiber line 22
2. def OAI.SharpRamseyFive.SelectedTuple.levelWindowStream line 24
3. abbrev OAI.SharpRamseyFive.SelectedTuple.LevelWindowSample line 41
4. def OAI.SharpRamseyFive.SelectedTuple.actualWindowEncoded line 44
5. def OAI.SharpRamseyFive.SelectedTuple.actualWindowPositions line 49
6. lemma OAI.SharpRamseyFive.SelectedTuple.actualWindow_loss_mean line 56
7. theorem OAI.SharpRamseyFive.SelectedTuple.actualWindow_stage line 74