OAI/Combinatorics/FiniteCircle/CircleWords.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiniteCircle.mem_maskTags line 9
  2. theorem OAI.FiniteCircle.length_maskTags line 15
  3. theorem OAI.FiniteCircle.nodup_maskTags line 19
  4. def OAI.FiniteCircle.maskLength line 43
  5. theorem OAI.FiniteCircle.length_maskWord line 47
  6. theorem OAI.FiniteCircle.shiftMaskState_zero line 69
  7. theorem OAI.FiniteCircle.shiftMaskState_add line 75
  8. theorem OAI.FiniteCircle.shiftMaskState_change_base line 83
  9. def OAI.FiniteCircle.maskRow line 91
  10. theorem OAI.FiniteCircle.length_maskRow line 96
  11. theorem OAI.FiniteCircle.segment_maskWord line 107
  12. theorem OAI.FiniteCircle.tag_get_maskWord line 118
  13. theorem OAI.FiniteCircle.fin_orderEmbedding_lower line 128
  14. theorem OAI.FiniteCircle.fin_orderEmbedding_upper line 140
  15. theorem OAI.FiniteCircle.threshold_neighborhood_card line 153
  16. theorem OAI.FiniteCircle.hamming_le_five_deficit line 167
  17. def OAI.FiniteCircle.halfBit line 220
  18. theorem OAI.FiniteCircle.zmod_val_sub_cases line 222
  19. theorem OAI.FiniteCircle.halfBit_interval line 234
  20. theorem OAI.FiniteCircle.halfBit_thresholds line 243
  21. def OAI.FiniteCircle.halfHamming line 273
  22. theorem OAI.FiniteCircle.halfHamming_symm line 276
  23. theorem OAI.FiniteCircle.halfHamming_translate line 283
  24. theorem OAI.FiniteCircle.halfHamming_zero_neg line 302
  25. theorem OAI.FiniteCircle.halfHamming_zero_small line 308
  26. theorem OAI.FiniteCircle.halfHamming_eq line 355
  27. theorem OAI.FiniteCircle.halfHamming_fin line 374
  28. theorem OAI.FiniteCircle.maskWord_zero_eq line 391
  29. theorem OAI.FiniteCircle.halfCircle_separation line 402
  30. def OAI.FiniteCircle.subcircle line 419
  31. theorem OAI.FiniteCircle.subcircle_natCast line 425
  32. theorem OAI.FiniteCircle.subcircle_val line 434
  33. theorem OAI.FiniteCircle.subcircle_injective line 440
  34. theorem OAI.FiniteCircle.add_ne_zero_of_coprime_orders line 453
  35. theorem OAI.FiniteCircle.PhaseCost.sub_le line 467
  36. theorem OAI.FiniteCircle.PhaseCost.le_pair line 470
  37. theorem OAI.FiniteCircle.PhaseCost.grid_pair_bound line 474
  38. theorem OAI.FiniteCircle.PhaseCost.prime_grid_bound line 485