OAI/Combinatorics/KMedian/Programs/GraphRunProgram.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.SparseGraph.Program.Input.state line 17
  2. def OAI.MetricKMedian.SparseGraph.Program.Input.start line 18
  3. theorem OAI.MetricKMedian.SparseGraph.Program.state_next line 20
  4. theorem OAI.MetricKMedian.SparseGraph.Program.state_iterate line 36
  5. def OAI.MetricKMedian.SparseGraph.Program.startProgram line 41
  6. def OAI.MetricKMedian.SparseGraph.Program.countProgram line 56
  7. theorem OAI.MetricKMedian.SparseGraph.Program.input_bounds line 60
  8. def OAI.MetricKMedian.SparseGraph.Program.supportBound line 94
  9. def OAI.MetricKMedian.SparseGraph.Program.heightBound line 95
  10. def OAI.MetricKMedian.SparseGraph.Program.graphSize line 96
  11. def OAI.MetricKMedian.SparseGraph.Program.sizeBound line 97
  12. def OAI.MetricKMedian.SparseGraph.Program.SPoly line 100
  13. def OAI.MetricKMedian.SparseGraph.Program.HPoly line 101
  14. def OAI.MetricKMedian.SparseGraph.Program.APoly line 102
  15. def OAI.MetricKMedian.SparseGraph.Program.sizePolynomial line 103
  16. theorem OAI.MetricKMedian.SparseGraph.Program.sizePolynomial_eval line 105
  17. theorem OAI.MetricKMedian.SparseGraph.Program.state_size line 109
  18. def OAI.MetricKMedian.SparseGraph.Program.runStateProgram line 156