OAI/Combinatorics/FiniteCircle/ExcludedDescent.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiniteCircle.PhaseSupported.neg line 9
  2. theorem OAI.FiniteCircle.circleCost_support_lower_pow line 14
  3. def OAI.FiniteCircle.pairResetBudget line 32
  4. theorem OAI.FiniteCircle.pairResetBudget_mono line 34
  5. theorem OAI.FiniteCircle.pairResetBudget_overflow line 39
  6. def OAI.FiniteCircle.pairDescentBound line 48
  7. theorem OAI.FiniteCircle.pairDescentBound_pos line 51
  8. theorem OAI.FiniteCircle.pairDescentBound_step line 55
  9. theorem OAI.FiniteCircle.pairDescentBound_base line 72
  10. theorem OAI.FiniteCircle.excluded_denominator_descent line 81
  11. theorem OAI.FiniteCircle.resetBudget_bound line 202
  12. theorem OAI.FiniteCircle.pairResetBudget_bound line 217
  13. theorem OAI.FiniteCircle.mask_budget_exponent line 232
  14. theorem OAI.FiniteCircle.excluded_budget_exponent line 241
  15. theorem OAI.FiniteCircle.four_eight_pow_le line 252
  16. theorem OAI.FiniteCircle.mask_descent_numeric line 264
  17. theorem OAI.FiniteCircle.excluded_descent_numeric line 289