OAI/Combinatorics/KMedianRecovery/Recovery/LengthPolynomial.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.PolyComputes.lengthPolynomial line 9
  2. lemma OAI.MetricKMedianRecovery.BitMachine.PolyComputes.length_bound line 11
  3. def OAI.MetricKMedianRecovery.BitMachine.WordList.cons line 18
  4. def OAI.MetricKMedianRecovery.BitMachine.WordList.encode line 19
  5. def OAI.MetricKMedianRecovery.BitMachine.WordList.head line 22
  6. def OAI.MetricKMedianRecovery.BitMachine.WordList.tail line 23
  7. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.head_cons line 24
  8. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.tail_cons line 26
  9. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.cons_ne_nil line 28
  10. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.length_cons line 29
  11. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.length_encode line 31
  12. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.length_le_encode line 36
  13. def OAI.MetricKMedianRecovery.BitMachine.WordList.head_computes line 38
  14. def OAI.MetricKMedianRecovery.BitMachine.WordList.tail_computes line 39
  15. def OAI.MetricKMedianRecovery.BitMachine.WordList.cons_computes line 41
  16. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.head_length line 43
  17. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.tail_length line 47
  18. def OAI.MetricKMedianRecovery.BitMachine.WordList.ReverseMap.step line 52
  19. def OAI.MetricKMedianRecovery.BitMachine.WordList.ReverseMap.step_computes line 56
  20. def OAI.MetricKMedianRecovery.BitMachine.WordList.ReverseMap.next line 65
  21. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.ReverseMap.data_next line 66
  22. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.ReverseMap.counter_next line 70
  23. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.ReverseMap.output_next line 77
  24. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.ReverseMap.length_next line 89
  25. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.ReverseMap.rank_next line 95
  26. def OAI.MetricKMedianRecovery.BitMachine.WordList.ReverseMap.growth line 108
  27. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.ReverseMap.iterate_bounds line 109
  28. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.ReverseMap.stop line 136
  29. def OAI.MetricKMedianRecovery.BitMachine.WordList.ReverseMap.loop_computes line 143
  30. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.ReverseMap.next_nil line 167
  31. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.ReverseMap.next_cons line 170
  32. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.ReverseMap.loop_exact line 174
  33. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.ReverseMap.loop_spec line 185
  34. def OAI.MetricKMedianRecovery.BitMachine.WordList.ReverseMap.run line 196
  35. def OAI.MetricKMedianRecovery.BitMachine.WordList.ReverseMap.run_computes line 199
  36. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.ReverseMap.run_encode line 202
  37. def OAI.MetricKMedianRecovery.BitMachine.WordList.reverse line 208
  38. def OAI.MetricKMedianRecovery.BitMachine.WordList.reverse_computes line 209
  39. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.reverse_encode line 211
  40. def OAI.MetricKMedianRecovery.BitMachine.WordList.mapWith line 213
  41. def OAI.MetricKMedianRecovery.BitMachine.WordList.mapWith_computes line 214
  42. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.mapWith_encode line 216