OAI/Combinatorics/IndependentSets/Machines/MachineExpanderFamilyBounds.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeCost line 11
  2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeCoefficient line 17
  3. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamilyBounds.wordLength_add_one_le line 21
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeCost_le line 32
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamilyBounds.vertexCount_monotone line 70
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamilyBounds.level_le_vertexCount line 76
  7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum line 88
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum_zero line 91
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum_succ line 94
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum_add line 98
  11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget line 103
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget_zero line 106
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget_succ line 109
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum_le line 115
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget_le line 142
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamilyBounds.paddedSize_le_succ_input line 156
  17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamilyBounds.inputCoefficient line 166
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget_at_boundedLevel_le line 169