OAI/Combinatorics/IndependentSets/Machines/MachineExpanderFamilyLoop.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.levelLoopCost line 12
2. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.levelLoopCost_prefix line 17
3. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.levelLoopCost_zero_start line 30
4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.levelLoopTapes line 35
5. structure OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.LevelLoopRun line 40
6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.familySingleStep line 50
7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.levelLoopInTime line 56
8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.singleFamilyStep line 94
9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.familyInTime line 100
10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.familyInOutputSizeTime line 136
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.baseDegree_cloud_growth line 147
12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.baseDegree_cloud_gt_one line 152
13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.baseDegree_positive line 156
14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.paddedFamilyInTime line 164