OAI/Combinatorics/KMedian/Process/RoundCountsProgram.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.FixedBatch.RationalParameters.RoundCountsProgram.Input line 17
  2. abbrev OAI.MetricKMedian.FixedBatch.RationalParameters.RoundCountsProgram.Raw line 23
  3. def OAI.MetricKMedian.FixedBatch.RationalParameters.RoundCountsProgram.Input.raw line 24
  4. abbrev OAI.MetricKMedian.FixedBatch.RationalParameters.RoundCountsProgram.Input.encode line 26
  5. def OAI.MetricKMedian.FixedBatch.RationalParameters.RoundCountsProgram.cap line 28
  6. theorem OAI.MetricKMedian.FixedBatch.RationalParameters.RoundCountsProgram.cap_poly line 29
  7. theorem OAI.MetricKMedian.FixedBatch.RationalParameters.RoundCountsProgram.cap_input line 30
  8. def OAI.MetricKMedian.FixedBatch.RationalParameters.RoundCountsProgram.valid line 34
  9. theorem OAI.MetricKMedian.FixedBatch.RationalParameters.RoundCountsProgram.valid_poly line 35
  10. theorem OAI.MetricKMedian.FixedBatch.RationalParameters.RoundCountsProgram.valid_input line 36
  11. def OAI.MetricKMedian.FixedBatch.RationalParameters.RoundCountsProgram.dummy line 42
  12. def OAI.MetricKMedian.FixedBatch.RationalParameters.RoundCountsProgram.Input.selection line 52
  13. def OAI.MetricKMedian.FixedBatch.RationalParameters.RoundCountsProgram.prepare line 59
  14. theorem OAI.MetricKMedian.FixedBatch.RationalParameters.RoundCountsProgram.prepare_poly line 62
  15. theorem OAI.MetricKMedian.FixedBatch.RationalParameters.RoundCountsProgram.prepare_input line 63
  16. def OAI.MetricKMedian.FixedBatch.RationalParameters.RoundCountsProgram.Input.result line 83
  17. def OAI.MetricKMedian.FixedBatch.RationalParameters.RoundCountsProgram.finish line 85
  18. theorem OAI.MetricKMedian.FixedBatch.RationalParameters.RoundCountsProgram.finish_poly line 86
  19. theorem OAI.MetricKMedian.FixedBatch.RationalParameters.RoundCountsProgram.finish_input line 87
  20. def OAI.MetricKMedian.FixedBatch.RationalParameters.RoundCountsProgram.program line 102