OAI/Combinatorics/FiniteCircle/Windows.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiniteCircle.segment_segment line 12
  2. theorem OAI.FiniteCircle.segment_append_left line 17
  3. theorem OAI.FiniteCircle.segment_append_right line 22
  4. theorem OAI.FiniteCircle.slide_segment_before line 27
  5. theorem OAI.FiniteCircle.slide_segment_after line 32
  6. theorem OAI.FiniteCircle.slide_segment_shift line 43
  7. def OAI.FiniteCircle.windows line 57
  8. theorem OAI.FiniteCircle.length_windows line 60
  9. theorem OAI.FiniteCircle.windows_before line 63
  10. theorem OAI.FiniteCircle.windows_after line 71
  11. theorem OAI.FiniteCircle.windows_shift line 79
  12. theorem OAI.FiniteCircle.block_location line 108
  13. theorem OAI.FiniteCircle.windows_nonexceptional line 127
  14. theorem OAI.FiniteCircle.lcs_append_ge line 141
  15. theorem OAI.FiniteCircle.deficit_append_le line 147
  16. theorem OAI.FiniteCircle.deficit_le_sum_blocks line 155