OAI/Combinatorics/KMedian/Programs/LastFractionProgram.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.RoundingList.Last.active line 13
  2. theorem OAI.MetricKMedian.RoundingList.Last.active_poly line 14
  3. theorem OAI.MetricKMedian.RoundingList.Last.active_list line 15
  4. theorem OAI.MetricKMedian.RoundingList.Last.first_list line 17
  5. def OAI.MetricKMedian.RoundingList.Last.probability line 25
  6. theorem OAI.MetricKMedian.RoundingList.Last.probability_poly line 26
  7. theorem OAI.MetricKMedian.RoundingList.Last.probability_list line 27
  8. def OAI.MetricKMedian.RoundingList.Last.endpoint line 36
  9. theorem OAI.MetricKMedian.RoundingList.Last.endpoint_poly line 39
  10. theorem OAI.MetricKMedian.RoundingList.Last.endpoint_list line 44
  11. def OAI.MetricKMedian.RoundingProgram.WeightedRound.State.last line 60
  12. def OAI.MetricKMedian.RoundingProgram.WeightedRound.lastRaw line 62
  13. theorem OAI.MetricKMedian.RoundingProgram.WeightedRound.lastRaw_poly line 65
  14. theorem OAI.MetricKMedian.RoundingProgram.WeightedRound.lastRaw_state line 71
  15. def OAI.MetricKMedian.RoundingProgram.WeightedRound.lastProgram line 78
  16. def OAI.MetricKMedian.RoundingProgram.WeightedRound.result line 83
  17. def OAI.MetricKMedian.RoundingProgram.WeightedRound.program line 85