OAI/Computability/Superstring/GroupSupply.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Superstring.ThreadArray.representative line 9
  2. theorem OAI.Superstring.ThreadArray.poly_representative line 12
  3. def OAI.Superstring.ThreadArray.groups line 19
  4. theorem OAI.Superstring.ThreadArray.poly_groups line 22
  5. theorem OAI.Superstring.ThreadArray.representative_spec line 29
  6. def OAI.Superstring.ThreadArray.repFin line 39
  7. theorem OAI.Superstring.ThreadArray.same_repFin line 44
  8. theorem OAI.Superstring.ThreadArray.representative_eq_iff line 50
  9. theorem OAI.Superstring.ThreadArray.representative_idem line 67
  10. abbrev OAI.Superstring.ThreadArray.Group line 72
  11. def OAI.Superstring.ThreadArray.groupOf line 75
  12. theorem OAI.Superstring.ThreadArray.groupOf_eq_iff line 80
  13. theorem OAI.Superstring.ThreadArray.compatible_groupOf line 95
  14. def OAI.Superstring.ThreadArray.collection line 108
  15. def OAI.Superstring.ThreadArray.phaseEquiv line 130
  16. def OAI.Superstring.ThreadArray.allPhaseEquiv line 138
  17. theorem OAI.Superstring.ThreadArray.collection_budget line 145
  18. theorem OAI.Superstring.ThreadArray.allPhaseEquiv_value line 154
  19. theorem OAI.Superstring.ThreadArray.phase_prefix_count line 160
  20. theorem OAI.Superstring.ThreadArray.collection_histogram line 180
  21. theorem OAI.Superstring.Hierarchical.LayerCollection.eq_of_alignment line 214
  22. abbrev OAI.Superstring.Hierarchical.LayerCollection.AlignedOccurrence line 221
  23. instance OAI.Superstring.Hierarchical.LayerCollection.(instance at line 224) line 224
  24. def OAI.Superstring.Hierarchical.LayerCollection.qualifyingLayer line 229
  25. theorem OAI.Superstring.Hierarchical.LayerCollection.qualifyingLayer_injective line 238
  26. theorem OAI.Superstring.Hierarchical.LayerCollection.aligned_card_le_qualifying line 257
  27. theorem OAI.Superstring.Hierarchical.LayerCollection.blocking_count line 268
  28. theorem OAI.Superstring.Hierarchical.LayerCollection.period_forces_matching line 280
  29. theorem OAI.Superstring.Hierarchical.LayerCollection.hard_case_record line 317
  30. theorem OAI.Superstring.Hierarchical.LayerCollection.recordSupply_of_histogram line 420
  31. def OAI.Superstring.Hierarchical.Layer.Record.normalize line 435

    Source documentation

    Only the period residue of a recipient offset is stored.

    def normalize (R : D.Record A) (per : Function.Periodic B (q : ℤ)) : D.Record A where
…
  32. theorem OAI.Superstring.Hierarchical.Layer.Record.normalize_text line 464
  33. theorem OAI.Superstring.Hierarchical.Layer.Record.bounds line 475
  34. abbrev OAI.Superstring.RecordCode.Code line 488
  35. def OAI.Superstring.RecordCode.offset line 489
  36. def OAI.Superstring.RecordCode.start line 490
  37. def OAI.Superstring.RecordCode.stop line 491
  38. def OAI.Superstring.RecordCode.check line 493
  39. theorem OAI.Superstring.RecordCode.check_record line 500
  40. theorem OAI.Superstring.RecordCode.poly_check line 510
  41. theorem OAI.Superstring.RecordCode.agree_of_word_eq line 521
  42. def OAI.Superstring.RecordCode.checkedRecord line 530
  43. def OAI.Superstring.RecordCode.pool line 539
  44. theorem OAI.Superstring.RecordCode.mem_pool line 543
  45. theorem OAI.Superstring.RecordCode.normalized_mem_pool line 562
  46. theorem OAI.Superstring.RecordCode.poly_pool line 572