OAI/Combinatorics/FiniteCircle/Separation.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteCircle.coordDist line 12
  2. theorem OAI.FiniteCircle.coordDist_nonneg line 15
  3. theorem OAI.FiniteCircle.coordDist_symm line 18
  4. theorem OAI.FiniteCircle.coordDist_triangle line 21
  5. def OAI.FiniteCircle.normalizeWord line 27
  6. theorem OAI.FiniteCircle.normalizeWord_val line 30
  7. theorem OAI.FiniteCircle.normalizeWord_deficit line 34
  8. def OAI.FiniteCircle.windowWords line 41
  9. theorem OAI.FiniteCircle.length_windowWords line 44
  10. theorem OAI.FiniteCircle.windowWords_ofFn line 47
  11. theorem OAI.FiniteCircle.windows_segment line 52
  12. theorem OAI.FiniteCircle.windowWords_segment line 61
  13. theorem OAI.FiniteCircle.cross_window_deficit line 66
  14. theorem OAI.FiniteCircle.exists_separating_scale line 81
  15. def OAI.FiniteCircle.partitionRate line 103
  16. theorem OAI.FiniteCircle.partitionRate_nonneg line 105
  17. theorem OAI.FiniteCircle.partition_collision_bound line 109
  18. theorem OAI.FiniteCircle.scale_collision_union line 121
  19. theorem OAI.FiniteCircle.block_histogram_lower line 126
  20. theorem OAI.FiniteCircle.normalized_slide_segment line 143
  21. theorem OAI.FiniteCircle.block_histogram_pairing line 155
  22. theorem OAI.FiniteCircle.fin_index_indicator_sum line 186
  23. theorem OAI.FiniteCircle.histogram_forward_bound line 196
  24. theorem OAI.FiniteCircle.histogram_slide_bound line 254
  25. theorem OAI.FiniteCircle.SlidePath.coordDist_le line 271