OAI/Computability/MaxCut/Games/GraphIterationBounds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

One polynomial bounds every actual intermediate encoding in the concrete logarithmic graph iteration. The linear recurrence is on graph size.

  1. def OAI.MaxCutGames.Foundations.Complexity.GraphIterationBounds.inputBits line 14
  2. def OAI.MaxCutGames.Foundations.Complexity.GraphIterationBounds.countedBits line 16
  3. def OAI.MaxCutGames.Foundations.Complexity.GraphIterationBounds.words line 18
  4. def OAI.MaxCutGames.Foundations.Complexity.GraphIterationBounds.count line 21
  5. def OAI.MaxCutGames.Foundations.Complexity.GraphIterationBounds.lengthPolynomial line 23
  6. theorem OAI.MaxCutGames.Foundations.Complexity.GraphIterationBounds.inputBits_le_countedBits line 26
  7. theorem OAI.MaxCutGames.Foundations.Complexity.GraphIterationBounds.size_le_inputBits line 30
  8. theorem OAI.MaxCutGames.Foundations.Complexity.GraphIterationBounds.count_le line 35
  9. theorem OAI.MaxCutGames.Foundations.Complexity.GraphIterationBounds.intermediate_size line 39
  10. theorem OAI.MaxCutGames.Foundations.Complexity.GraphIterationBounds.intermediate_bits line 47
  11. def OAI.MaxCutGames.Foundations.Complexity.GraphIterationBounds.runtimePolynomial line 63
  12. theorem OAI.MaxCutGames.Foundations.Complexity.GraphIterationBounds.runtimePolynomial_eval line 67