OAI/Combinatorics/IndependentSets/Expansion/PoweringPolynomialBudget.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringPolynomialBudget.preBudget line 10
  2. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringPolynomialBudget.finishBudget line 14
  3. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringPolynomialBudget.totalBudget line 19
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringPolynomialBudget.preBudget_mono_vertices line 24
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringPolynomialBudget.finishBudget_mono line 31
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringPolynomialBudget.totalBudget_mono_vertices line 46
  7. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringPolynomialBudget.rowTime line 55
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringPolynomialBudget.rowTime_eval line 62
  9. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringPolynomialBudget.vertexTime line 68
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringPolynomialBudget.vertexTime_eval line 71
  11. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringPolynomialBudget.preTime line 76
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringPolynomialBudget.preTime_eval line 80
  13. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringPolynomialBudget.time line 85
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringPolynomialBudget.time_eval line 93
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringPolynomialBudget.totalBudget_le_time line 99
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringPolynomialBudget.setup_loop_finish_le_time line 106
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringPolynomialBudget.execution_budget_le_time line 119
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringPolynomialBudget.graph_totalBudget_le_time line 132