OAI/Combinatorics/KMedian/Process/PhysicalRoundProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.RationalPhysicalKernel.RoundProgram.Raw line 18
  2. def OAI.MetricKMedian.RationalPhysicalKernel.RoundProgram.ctxRaw line 19
  3. abbrev OAI.MetricKMedian.RationalPhysicalKernel.RoundProgram.ctxEncode line 20
  4. def OAI.MetricKMedian.RationalPhysicalKernel.RoundProgram.ctxInputs line 22
  5. def OAI.MetricKMedian.RationalPhysicalKernel.RoundProgram.attach line 24
  6. theorem OAI.MetricKMedian.RationalPhysicalKernel.RoundProgram.attach_poly line 27
  7. theorem OAI.MetricKMedian.RationalPhysicalKernel.RoundProgram.attach_input line 33
  8. def OAI.MetricKMedian.RationalPhysicalKernel.RoundProgram.graphProgram line 39
  9. def OAI.MetricKMedian.RationalPhysicalKernel.RoundProgram.inputsProgram line 44
  10. def OAI.MetricKMedian.RationalPhysicalKernel.RoundProgram.dummy line 56
  11. def OAI.MetricKMedian.RationalPhysicalKernel.RoundProgram.ctxLaw line 73
  12. def OAI.MetricKMedian.RationalPhysicalKernel.RoundProgram.ctxResult line 75
  13. def OAI.MetricKMedian.RationalPhysicalKernel.RoundProgram.program line 78
  14. theorem OAI.MetricKMedian.RationalPhysicalKernel.RoundProgram.law_step line 93