OAI/Combinatorics/FiniteCircle/MaskSeparation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FiniteCircle.MaskResidues line 9
  2. def OAI.FiniteCircle.maskPhaseHom line 11
  3. theorem OAI.FiniteCircle.maskPhaseHom_natCast line 20
  4. theorem OAI.FiniteCircle.sum_fin_zmod line 34
  5. def OAI.FiniteCircle.maskCost line 45
  6. theorem OAI.FiniteCircle.maskCost_le_half line 53
  7. theorem OAI.FiniteCircle.card_maskTag line 63
  8. theorem OAI.FiniteCircle.mask_average_formula line 67
  9. theorem OAI.FiniteCircle.mask_active_average_lower line 85
  10. theorem OAI.FiniteCircle.mask_inactive_average_lower line 141
  11. theorem OAI.FiniteCircle.mask_minimizer_options line 191
  12. theorem OAI.FiniteCircle.deficit_cast line 215
  13. theorem OAI.FiniteCircle.deficit_taggedRow_lower line 218
  14. theorem OAI.FiniteCircle.maskLength_pos line 228
  15. theorem OAI.FiniteCircle.mask_separation line 240