OAI/Combinatorics/FiniteCircle/PhaseCost.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteCircle.circleCost line 9
  2. theorem OAI.FiniteCircle.circleCost_zero line 11
  3. theorem OAI.FiniteCircle.circleCost_nonneg line 14
  4. theorem OAI.FiniteCircle.circleCost_neg line 18
  5. theorem OAI.FiniteCircle.circleCost_add_le line 21
  6. theorem OAI.FiniteCircle.circleCost_le_half line 29
  7. theorem OAI.FiniteCircle.circleCost_pos line 38
  8. theorem OAI.FiniteCircle.circleCost_order_lower line 45
  9. structure OAI.FiniteCircle.PhaseCost line 63
  10. instance OAI.FiniteCircle.(instance at line 70) line 70
  11. def OAI.FiniteCircle.circlePhaseCost line 72
  12. def OAI.FiniteCircle.PhaseCost.average line 78
  13. def OAI.FiniteCircle.PhaseCost.infAverage line 81
  14. theorem OAI.FiniteCircle.PhaseCost.infAverage_le line 84
  15. theorem OAI.FiniteCircle.PhaseCost.exists_average_eq line 88
  16. theorem OAI.FiniteCircle.PhaseCost.infAverage_nonneg line 93
  17. theorem OAI.FiniteCircle.PhaseCost.average_zero_mask line 100
  18. theorem OAI.FiniteCircle.PhaseCost.infAverage_le_self line 106
  19. theorem OAI.FiniteCircle.PhaseCost.infAverage_zero line 110
  20. theorem OAI.FiniteCircle.PhaseCost.average_neg line 119
  21. theorem OAI.FiniteCircle.PhaseCost.infAverage_neg line 128
  22. theorem OAI.FiniteCircle.PhaseCost.average_add_le line 137
  23. theorem OAI.FiniteCircle.PhaseCost.infAverage_add_le line 150
  24. def OAI.FiniteCircle.PhaseCost.step line 157