OAI/Combinatorics/KMedian/Rounding/SignedListOperations.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.RoundingList.square line 13
  2. theorem OAI.MetricKMedian.RoundingList.square_poly line 15
  3. theorem OAI.MetricKMedian.RoundingList.ofFn_product line 22
  4. theorem OAI.MetricKMedian.RoundingList.square_list line 42
  5. def OAI.MetricKMedian.RoundingList.Signed.valid line 51
  6. def OAI.MetricKMedian.RoundingList.Signed.index line 54
  7. def OAI.MetricKMedian.RoundingList.Signed.pair line 55
  8. def OAI.MetricKMedian.RoundingList.Signed.active line 56
  9. def OAI.MetricKMedian.RoundingList.Signed.ratio line 57
  10. def OAI.MetricKMedian.RoundingList.Signed.probability line 59
  11. def OAI.MetricKMedian.RoundingList.Signed.endpoint line 65
  12. theorem OAI.MetricKMedian.RoundingList.Signed.valid_list line 70
  13. theorem OAI.MetricKMedian.RoundingList.Signed.active_list line 78
  14. theorem OAI.MetricKMedian.RoundingList.Signed.index_list line 90
  15. theorem OAI.MetricKMedian.RoundingList.Signed.pair_list line 104
  16. theorem OAI.MetricKMedian.RoundingList.Signed.probability_list line 108
  17. theorem OAI.MetricKMedian.RoundingList.Signed.endpoint_list line 117
  18. theorem OAI.MetricKMedian.RoundingList.Signed.valid_poly line 127
  19. theorem OAI.MetricKMedian.RoundingList.Signed.index_poly line 131
  20. theorem OAI.MetricKMedian.RoundingList.Signed.pair_poly line 134
  21. theorem OAI.MetricKMedian.RoundingList.Signed.active_poly line 135
  22. theorem OAI.MetricKMedian.RoundingList.Signed.ratio_poly line 136
  23. theorem OAI.MetricKMedian.RoundingList.Signed.probability_poly line 137
  24. theorem OAI.MetricKMedian.RoundingList.Signed.endpoint_poly line 138