OAI/Combinatorics/KMedian/Process/BatchActionArrays.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.RationalBatchData.ActionArrays.erase line 16
  2. def OAI.MetricKMedian.RationalBatchData.ActionArrays.bal line 19
  3. def OAI.MetricKMedian.RationalBatchData.ActionArrays.overlap line 21
  4. def OAI.MetricKMedian.RationalBatchData.ActionArrays.conflict line 23
  5. def OAI.MetricKMedian.RationalBatchData.ActionArrays.bias line 25
  6. theorem OAI.MetricKMedian.RationalBatchData.ActionArrays.erase_poly line 28
  7. theorem OAI.MetricKMedian.RationalBatchData.ActionArrays.bal_poly line 33
  8. theorem OAI.MetricKMedian.RationalBatchData.ActionArrays.overlap_poly line 38
  9. theorem OAI.MetricKMedian.RationalBatchData.ActionArrays.conflict_poly line 42
  10. theorem OAI.MetricKMedian.RationalBatchData.ActionArrays.bias_poly line 44
  11. theorem OAI.MetricKMedian.RationalBatchData.ActionArrays.code_light line 47
  12. theorem OAI.MetricKMedian.RationalBatchData.ActionArrays.erase_code line 52
  13. theorem OAI.MetricKMedian.RationalBatchData.ActionArrays.bal_code line 69
  14. theorem OAI.MetricKMedian.RationalBatchData.ActionArrays.overlap_view line 83
  15. theorem OAI.MetricKMedian.RationalBatchData.ActionArrays.conflict_code line 90
  16. theorem OAI.MetricKMedian.RationalBatchData.ActionArrays.bias_code line 101
  17. abbrev OAI.MetricKMedian.RationalBatchData.ActionArrays.Raw line 108
  18. def OAI.MetricKMedian.RationalBatchData.ActionArrays.data line 110
  19. theorem OAI.MetricKMedian.RationalBatchData.ActionArrays.data_poly line 114
  20. theorem OAI.MetricKMedian.RationalBatchData.ActionArrays.data_view line 128