OAI/Combinatorics/KMedian/Process/CountRunProgram.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.SparseCounts.Program.Input.state line 17
  2. def OAI.MetricKMedian.SparseCounts.Program.Input.start line 18
  3. theorem OAI.MetricKMedian.SparseCounts.Program.state_next line 20
  4. theorem OAI.MetricKMedian.SparseCounts.Program.state_iterate line 36
  5. def OAI.MetricKMedian.SparseCounts.Program.startProgram line 41
  6. def OAI.MetricKMedian.SparseCounts.Program.countProgram line 56
  7. theorem OAI.MetricKMedian.SparseCounts.Program.input_bounds line 60
  8. theorem OAI.MetricKMedian.SparseCounts.Program.entry_bound line 94
  9. def OAI.MetricKMedian.SparseCounts.Program.supportBound line 116
  10. def OAI.MetricKMedian.SparseCounts.Program.heightBound line 117
  11. def OAI.MetricKMedian.SparseCounts.Program.graphSize line 118
  12. def OAI.MetricKMedian.SparseCounts.Program.sizeBound line 119
  13. def OAI.MetricKMedian.SparseCounts.Program.SPoly line 122
  14. def OAI.MetricKMedian.SparseCounts.Program.HPoly line 123
  15. def OAI.MetricKMedian.SparseCounts.Program.APoly line 124
  16. def OAI.MetricKMedian.SparseCounts.Program.sizePolynomial line 125
  17. theorem OAI.MetricKMedian.SparseCounts.Program.sizePolynomial_eval line 127
  18. theorem OAI.MetricKMedian.SparseCounts.Program.state_size line 131
  19. def OAI.MetricKMedian.SparseCounts.Program.runStateProgram line 183