OAI/Combinatorics/KMedian/Hardness/ProjectionEncoding.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.Coverage.ProjectionRaw line 14
  2. abbrev OAI.MetricKMedian.Coverage.BlockCode line 15
  3. def OAI.MetricKMedian.Coverage.ProjectionRaw.lefts line 19
  4. def OAI.MetricKMedian.Coverage.ProjectionRaw.rights line 20
  5. def OAI.MetricKMedian.Coverage.ProjectionRaw.edge line 22
  6. def OAI.MetricKMedian.Coverage.ProjectionRaw.test line 25
  7. def OAI.MetricKMedian.Coverage.ProjectionRaw.incident line 29
  8. theorem OAI.MetricKMedian.Coverage.ProjectionRaw.lefts_poly line 32
  9. theorem OAI.MetricKMedian.Coverage.ProjectionRaw.rights_poly line 34
  10. theorem OAI.MetricKMedian.Coverage.ProjectionRaw.edge_poly line 36
  11. theorem OAI.MetricKMedian.Coverage.ProjectionRaw.test_poly line 38
  12. theorem OAI.MetricKMedian.Coverage.ProjectionRaw.incident_poly line 41
  13. def OAI.MetricKMedian.Coverage.ProjectionRaw.blocks line 50
  14. def OAI.MetricKMedian.Coverage.ProjectionRaw.table line 55
  15. theorem OAI.MetricKMedian.Coverage.ProjectionRaw.table_poly line 59
  16. def OAI.MetricKMedian.Coverage.ProjectionRaw.bytes line 80
  17. theorem OAI.MetricKMedian.Coverage.ProjectionRaw.bytes_poly line 85
  18. def OAI.MetricKMedian.Coverage.ProjectionRaw.program line 90
  19. def OAI.MetricKMedian.Coverage.ProjectionInput.raw line 100
  20. def OAI.MetricKMedian.Coverage.ProjectionInput.encode line 105
  21. theorem OAI.MetricKMedian.Coverage.ProjectionInput.raw_lefts line 107
  22. theorem OAI.MetricKMedian.Coverage.ProjectionInput.raw_rights line 109
  23. theorem OAI.MetricKMedian.Coverage.ProjectionInput.raw_edge line 112
  24. theorem OAI.MetricKMedian.Coverage.ProjectionInput.raw_test line 118
  25. theorem OAI.MetricKMedian.Coverage.ProjectionInput.raw_incident line 128
  26. theorem OAI.MetricKMedian.Coverage.ProjectionInput.ofFn_product line 147
  27. theorem OAI.MetricKMedian.Coverage.ProjectionInput.client_block line 162
  28. theorem OAI.MetricKMedian.Coverage.ProjectionInput.table_correct line 167
  29. theorem OAI.MetricKMedian.Coverage.ProjectionInput.bytes_correct line 192
  30. def OAI.MetricKMedian.Coverage.ProjectionInput.coverageProgram line 198
  31. theorem OAI.MetricKMedian.Coverage.ProjectionInput.coverage_finite_poly line 203