OAI/Combinatorics/KMedian/Process/RoundingUniformStep.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.RoundingList.features line 14
  2. def OAI.MetricKMedian.RoundingList.dimensions line 15
  3. theorem OAI.MetricKMedian.RoundingList.features_poly line 17
  4. theorem OAI.MetricKMedian.RoundingList.dimensions_poly line 24
  5. theorem OAI.MetricKMedian.RoundingList.dimensions_list line 32
  6. theorem OAI.MetricKMedian.RoundingList.features_list line 37
  7. abbrev OAI.MetricKMedian.RoundingProgram.Row line 59
  8. abbrev OAI.MetricKMedian.RoundingProgram.erow line 60
  9. structure OAI.MetricKMedian.RoundingProgram.State line 62
  10. def OAI.MetricKMedian.RoundingProgram.State.encode line 68
  11. def OAI.MetricKMedian.RoundingProgram.State.raw line 70
  12. theorem OAI.MetricKMedian.RoundingProgram.encodeList_map line 73
  13. theorem OAI.MetricKMedian.RoundingProgram.State.encode_raw line 79
  14. def OAI.MetricKMedian.RoundingProgram.State.branch line 84
  15. def OAI.MetricKMedian.RoundingProgram.State.compressionInput line 90
  16. def OAI.MetricKMedian.RoundingProgram.State.compress line 92
  17. def OAI.MetricKMedian.RoundingProgram.State.step line 94
  18. def OAI.MetricKMedian.RoundingProgram.probability line 96
  19. def OAI.MetricKMedian.RoundingProgram.endpoint line 98
  20. def OAI.MetricKMedian.RoundingProgram.probabilityProgram line 101
  21. def OAI.MetricKMedian.RoundingProgram.endpointProgram line 105
  22. def OAI.MetricKMedian.RoundingProgram.branchRawProgram line 110