OAI/Combinatorics/KMedian/Process/RoundingRunProgram.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.RoundingProgram.Input line 15
  2. def OAI.MetricKMedian.RoundingProgram.Input.raw line 22
  3. abbrev OAI.MetricKMedian.RoundingProgram.Input.encode line 23
  4. def OAI.MetricKMedian.RoundingProgram.Input.start line 24
  5. def OAI.MetricKMedian.RoundingProgram.Input.run line 25
  6. theorem OAI.MetricKMedian.RoundingProgram.input_iterate line 29
  7. def OAI.MetricKMedian.RoundingProgram.startProgram line 37
  8. def OAI.MetricKMedian.RoundingProgram.countProgram line 48
  9. theorem OAI.MetricKMedian.RoundingProgram.input_bounds line 52
  10. def OAI.MetricKMedian.RoundingProgram.heightBound line 69
  11. def OAI.MetricKMedian.RoundingProgram.coordinateBound line 70
  12. def OAI.MetricKMedian.RoundingProgram.supportBound line 71
  13. def OAI.MetricKMedian.RoundingProgram.stateBound line 72
  14. def OAI.MetricKMedian.RoundingProgram.CPoly line 76
  15. def OAI.MetricKMedian.RoundingProgram.NPoly line 77
  16. def OAI.MetricKMedian.RoundingProgram.HPoly line 78
  17. def OAI.MetricKMedian.RoundingProgram.statePolynomial line 81
  18. theorem OAI.MetricKMedian.RoundingProgram.statePolynomial_eval line 84
  19. theorem OAI.MetricKMedian.RoundingProgram.run_size line 88
  20. def OAI.MetricKMedian.RoundingProgram.runProgram line 130