OAI/Combinatorics/KMedianRecovery/Recovery/Copies.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.RepeatedAppend.copies line 10
  2. lemma OAI.MetricKMedianRecovery.BitMachine.RepeatedAppend.length_copies line 13
  3. def OAI.MetricKMedianRecovery.BitMachine.RepeatedAppend.step line 18
  4. def OAI.MetricKMedianRecovery.BitMachine.RepeatedAppend.step_computes line 21
  5. def OAI.MetricKMedianRecovery.BitMachine.RepeatedAppend.next line 29
  6. lemma OAI.MetricKMedianRecovery.BitMachine.RepeatedAppend.data_next line 30
  7. lemma OAI.MetricKMedianRecovery.BitMachine.RepeatedAppend.counter_next line 34
  8. lemma OAI.MetricKMedianRecovery.BitMachine.RepeatedAppend.output_next line 38
  9. lemma OAI.MetricKMedianRecovery.BitMachine.RepeatedAppend.length_next line 42
  10. lemma OAI.MetricKMedianRecovery.BitMachine.RepeatedAppend.rank_next line 48
  11. lemma OAI.MetricKMedianRecovery.BitMachine.RepeatedAppend.iterate_bounds line 59
  12. lemma OAI.MetricKMedianRecovery.BitMachine.RepeatedAppend.stop line 81
  13. def OAI.MetricKMedianRecovery.BitMachine.RepeatedAppend.loop_computes line 87
  14. lemma OAI.MetricKMedianRecovery.BitMachine.RepeatedAppend.next_nil line 103
  15. lemma OAI.MetricKMedianRecovery.BitMachine.RepeatedAppend.next_cons line 105
  16. lemma OAI.MetricKMedianRecovery.BitMachine.RepeatedAppend.loop_spec line 109
  17. def OAI.MetricKMedianRecovery.BitMachine.RepeatedAppend.run line 115
  18. def OAI.MetricKMedianRecovery.BitMachine.RepeatedAppend.run_computes line 116
  19. lemma OAI.MetricKMedianRecovery.BitMachine.RepeatedAppend.run_pair line 123
  20. structure OAI.MetricKMedianRecovery.BitMachine.PolynomialCounter line 128
  21. def OAI.MetricKMedianRecovery.BitMachine.PolynomialCounter.constant line 133
  22. def OAI.MetricKMedianRecovery.BitMachine.PolynomialCounter.identity line 137
  23. def OAI.MetricKMedianRecovery.BitMachine.PolynomialCounter.add line 141
  24. def OAI.MetricKMedianRecovery.BitMachine.PolynomialCounter.mul line 146
  25. theorem OAI.MetricKMedianRecovery.BitMachine.PolynomialCounter.nonempty line 154
  26. def OAI.MetricKMedianRecovery.BitMachine.PolynomialCounter.choose line 162
  27. def OAI.MetricKMedianRecovery.BitMachine.BoundedIteration.polynomialRun line 167
  28. def OAI.MetricKMedianRecovery.BitMachine.BoundedIteration.polynomialRun_computes line 169
  29. lemma OAI.MetricKMedianRecovery.BitMachine.BoundedIteration.polynomialRun_eq line 176