OAI/Combinatorics/FiniteCircle/MaskDescent.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteCircle.PhaseSupported line 9
  2. theorem OAI.FiniteCircle.primes_coprime_prod line 12
  3. theorem OAI.FiniteCircle.nsmul_zero_of_dvd line 24
  4. theorem OAI.FiniteCircle.PhaseSupported.mono line 29
  5. theorem OAI.FiniteCircle.PhaseSupported.add line 33
  6. theorem OAI.FiniteCircle.phase_add_supported_ne_zero line 41
  7. theorem OAI.FiniteCircle.support_subcircle line 47
  8. theorem OAI.FiniteCircle.support_mask_sum line 53
  9. theorem OAI.FiniteCircle.circleCost_support_lower line 68
  10. def OAI.FiniteCircle.resetBudget line 86
  11. theorem OAI.FiniteCircle.resetBudget_mono line 88
  12. theorem OAI.FiniteCircle.resetBudget_overflow line 93
  13. def OAI.FiniteCircle.descentBound line 103
  14. theorem OAI.FiniteCircle.descentBound_pos line 106
  15. theorem OAI.FiniteCircle.descentBound_step line 111
  16. theorem OAI.FiniteCircle.support_card_pos line 129
  17. def OAI.FiniteCircle.LowerFresh line 136
  18. theorem OAI.FiniteCircle.descentBound_base line 139
  19. theorem OAI.FiniteCircle.mask_denominator_descent line 148