OAI/Combinatorics/KMedian/Process/RoundingStateCompiler.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.RoundingProgram.vectorData line 13
  2. theorem OAI.MetricKMedian.RoundingProgram.vectorData_branch line 16
  3. theorem OAI.MetricKMedian.RoundingProgram.branch_raw line 29
  4. def OAI.MetricKMedian.RoundingProgram.branchProgram line 53
  5. def OAI.MetricKMedian.RoundingProgram.compressionInputProgram line 57
  6. def OAI.MetricKMedian.RoundingProgram.statesProgram line 73
  7. def OAI.MetricKMedian.RoundingProgram.weightsProgram line 76
  8. theorem OAI.MetricKMedian.RoundingProgram.trimData_map line 80
  9. theorem OAI.MetricKMedian.RoundingProgram.trim_encode_raw line 86
  10. def OAI.MetricKMedian.RoundingProgram.compressProgram line 93
  11. def OAI.MetricKMedian.RoundingProgram.stepProgram line 106