OAI/Combinatorics/KMedian/Binary/BinaryIterations.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Binary.Iteration.iterates line 16
  2. theorem OAI.MetricKMedian.Binary.Iteration.iterates_eq line 20
  3. abbrev OAI.MetricKMedian.Binary.Iteration.State line 28
  4. def OAI.MetricKMedian.Binary.Iteration.enc line 29
  5. def OAI.MetricKMedian.Binary.Iteration.body line 30
  6. def OAI.MetricKMedian.Binary.Iteration.program line 33
  7. def OAI.MetricKMedian.Binary.Iteration.bound line 47
  8. theorem OAI.MetricKMedian.Binary.Iteration.state_size line 49
  9. theorem OAI.MetricKMedian.Binary.Iteration.run line 58
  10. def OAI.MetricKMedian.Binary.PolyProgram.iteratesFrom line 85