OAI/Combinatorics/FiniteCircle/OffsetRecovery.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiniteCircle.WordMatching.common_offset_duplicate_loss line 14
  2. theorem OAI.FiniteCircle.WordMatching.common_offset_duplicates_card line 59
  3. def OAI.FiniteCircle.WordMatching.matchedAt line 100
  4. instance OAI.FiniteCircle.WordMatching.matchedAtDecidable line 103
  5. def OAI.FiniteCircle.WordMatching.partnerAt line 106
  6. theorem OAI.FiniteCircle.WordMatching.partnerAt_eq line 109
  7. theorem OAI.FiniteCircle.WordMatching.matchedAt_block line 117
  8. theorem OAI.FiniteCircle.WordMatching.unmatched_offsets_card_le line 127
  9. def OAI.FiniteCircle.WordMatching.duplicateAt line 152
  10. instance OAI.FiniteCircle.WordMatching.duplicateAtDecidable line 156
  11. theorem OAI.FiniteCircle.WordMatching.duplicate_offsets_card_le line 161
  12. theorem OAI.FiniteCircle.sum_card_filters_swap line 181
  13. theorem OAI.FiniteCircle.WordMatching.sum_omitted_offsets_le line 190
  14. theorem OAI.FiniteCircle.WordMatching.sum_duplicate_offsets_le line 209
  15. theorem OAI.FiniteCircle.WordMatching.offset_deficit_le line 242
  16. theorem OAI.FiniteCircle.WordMatching.averaged_offset_recovery line 291
  17. def OAI.FiniteCircle.WordMatching.offsetGood line 315
  18. theorem OAI.FiniteCircle.WordMatching.offsetGood_subset line 319
  19. theorem OAI.FiniteCircle.WordMatching.offsetGood_span line 322
  20. theorem OAI.FiniteCircle.WordMatching.offsetGood_bad_cost line 333
  21. theorem OAI.FiniteCircle.offset_deficit_lower line 374