OAI/Combinatorics/KMedian/Process/RoundingListOperations.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.RoundingList.Row line 14
  2. abbrev OAI.MetricKMedian.RoundingList.er line 15
  3. def OAI.MetricKMedian.RoundingList.frac line 17
  4. def OAI.MetricKMedian.RoundingList.indices line 18
  5. def OAI.MetricKMedian.RoundingList.fractional line 19
  6. def OAI.MetricKMedian.RoundingList.first line 20
  7. def OAI.MetricKMedian.RoundingList.second line 21
  8. def OAI.MetricKMedian.RoundingList.active line 22
  9. def OAI.MetricKMedian.RoundingList.ratio line 23
  10. def OAI.MetricKMedian.RoundingList.up line 25
  11. def OAI.MetricKMedian.RoundingList.down line 26
  12. def OAI.MetricKMedian.RoundingList.move line 27
  13. def OAI.MetricKMedian.RoundingList.probability line 29
  14. def OAI.MetricKMedian.RoundingList.endpoint line 35
  15. theorem OAI.MetricKMedian.RoundingList.range_finRange line 40
  16. theorem OAI.MetricKMedian.RoundingList.fractional_list line 45
  17. theorem OAI.MetricKMedian.RoundingList.active_list line 55
  18. theorem OAI.MetricKMedian.RoundingList.findIdx_min line 59
  19. theorem OAI.MetricKMedian.RoundingList.first_list line 74
  20. theorem OAI.MetricKMedian.RoundingList.second_list line 83
  21. theorem OAI.MetricKMedian.RoundingList.get_point line 99
  22. theorem OAI.MetricKMedian.RoundingList.up_list line 100
  23. theorem OAI.MetricKMedian.RoundingList.down_list line 102
  24. theorem OAI.MetricKMedian.RoundingList.move_list line 104
  25. theorem OAI.MetricKMedian.RoundingList.probability_list line 111
  26. theorem OAI.MetricKMedian.RoundingList.endpoint_list line 120
  27. theorem OAI.MetricKMedian.RoundingList.frac_poly line 130
  28. theorem OAI.MetricKMedian.RoundingList.indices_poly line 131
  29. theorem OAI.MetricKMedian.RoundingList.fractional_poly line 132
  30. theorem OAI.MetricKMedian.RoundingList.first_poly line 135
  31. theorem OAI.MetricKMedian.RoundingList.second_poly line 138
  32. theorem OAI.MetricKMedian.RoundingList.active_poly line 144
  33. theorem OAI.MetricKMedian.RoundingList.ratio_poly line 145
  34. theorem OAI.MetricKMedian.RoundingList.up_poly line 146
  35. theorem OAI.MetricKMedian.RoundingList.down_poly line 147
  36. theorem OAI.MetricKMedian.RoundingList.move_poly line 148
  37. theorem OAI.MetricKMedian.RoundingList.probability_poly line 153
  38. theorem OAI.MetricKMedian.RoundingList.endpoint_poly line 154