OAI/NumberTheory/Ostmann/Construction/ScheduledPageAvoidance.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.selectedTailCellPrimes_avoids line 10
2. theorem OAI.Ostmann.completedCompensationSets_avoids line 16
3. theorem OAI.Ostmann.scheduledRegularPrimeSets_avoids line 21
4. theorem OAI.Ostmann.selected_schedule_avoids_giant_page line 29
5. theorem OAI.Ostmann.FrozenInitialSpectatorData.avoids_giant_page line 45
6. theorem OAI.Ostmann.FrozenInitialSpectatorData.avoids_bulk_page line 54