OAI/Combinatorics/KMedian/Hardness/Encoding.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.Coverage.Raw line 13
  2. abbrev OAI.MetricKMedian.Coverage.Raw.m line 16
  3. abbrev OAI.MetricKMedian.Coverage.Raw.n line 17
  4. abbrev OAI.MetricKMedian.Coverage.Raw.k line 18
  5. abbrev OAI.MetricKMedian.Coverage.Raw.table line 19
  6. def OAI.MetricKMedian.Coverage.Raw.parse line 21
  7. theorem OAI.MetricKMedian.Coverage.Raw.parse_poly line 27
  8. def OAI.MetricKMedian.Coverage.Raw.indices line 29
  9. theorem OAI.MetricKMedian.Coverage.Raw.indices_poly line 32
  10. def OAI.MetricKMedian.Coverage.Raw.bitsProgram line 45
  11. theorem OAI.MetricKMedian.Coverage.Raw.bits_poly line 48
  12. theorem OAI.MetricKMedian.Coverage.Raw.encodeNat_poly line 50
  13. def OAI.MetricKMedian.Coverage.Raw.entry line 56
  14. theorem OAI.MetricKMedian.Coverage.Raw.entry_poly line 66
  15. def OAI.MetricKMedian.Coverage.Raw.medianBytes line 69
  16. theorem OAI.MetricKMedian.Coverage.Raw.medianBytes_poly line 75
  17. def OAI.MetricKMedian.Coverage.Raw.parsedProgram line 107
  18. def OAI.MetricKMedian.Coverage.Raw.typedMedianProgram line 112
  19. def OAI.MetricKMedian.Coverage.Raw.medianProgram line 118
  20. def OAI.MetricKMedian.Coverage.Input.raw line 126
  21. theorem OAI.MetricKMedian.Coverage.Input.parse_encode line 129
  22. theorem OAI.MetricKMedian.Coverage.Input.table_length line 132
  23. theorem OAI.MetricKMedian.Coverage.Input.n_pos line 135
  24. theorem OAI.MetricKMedian.Coverage.Input.indices_raw line 137
  25. theorem OAI.MetricKMedian.Coverage.Input.raw_m line 146
  26. theorem OAI.MetricKMedian.Coverage.Input.raw_n line 147
  27. theorem OAI.MetricKMedian.Coverage.Input.raw_k line 148
  28. theorem OAI.MetricKMedian.Coverage.Input.table_flatten line 150
  29. theorem OAI.MetricKMedian.Coverage.Input.table_get line 172
  30. theorem OAI.MetricKMedian.Coverage.Input.client_val line 188
  31. theorem OAI.MetricKMedian.Coverage.Input.facility_val line 189
  32. theorem OAI.MetricKMedian.Coverage.Input.entry_point line 191
  33. theorem OAI.MetricKMedian.Coverage.Input.entry_distance line 224
  34. theorem OAI.MetricKMedian.Coverage.Input.mem_clients_iff line 229
  35. theorem OAI.MetricKMedian.Coverage.Input.mem_facilities_iff line 246
  36. theorem OAI.MetricKMedian.Coverage.Input.medianBytes_correct line 263
  37. def OAI.MetricKMedian.Coverage.Input.reductionProgram line 286
  38. theorem OAI.MetricKMedian.Coverage.Input.reduction_finite_poly line 290