OAI/Combinatorics/KMedianRecovery/Branching/CategoricalOutput.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.outputPack line 13
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.output line 16
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.output_computes line 19
  4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.output_pack line 24
  5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.output_correct line 36
  6. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Tape.M line 48
  7. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Tape.K line 49
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Tape.tensors line 51
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Tape.split line 63
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Tape.tensorPair line 67
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Tape.layout line 69
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Tape.raw line 72
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Tape.tensorPair_raw line 74
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Tape.raw_layout line 80
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Tape.raw_left_length line 84
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Tape.raw_right_length line 87
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Tape.parsed_left line 90
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Tape.parsed_right line 93
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Tape.layout_average line 96
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.pack line 105
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.bword line 106
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.bword_computes line 108
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.bword_pack line 111
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.tbits line 115
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.tbits_computes line 116
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.tbits_pack line 118
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.qnext line 121
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.anext line 122
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.qnext_computes line 123
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.anext_computes line 124
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.factor line 126
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.factor_computes line 127
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.lbits line 132
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.lbits_computes line 133
  35. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.lbits_pack line 137
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.capPoly line 141
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.cap line 142
  38. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.cap_length line 143
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.unary line 146
  40. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.unary_computes line 147
  41. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.unary_eq line 149
  42. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.dimensions line 153
  43. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.sample_bound line 157
  44. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.tword line 170
  45. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.lword line 171
  46. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.tword_computes line 172
  47. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.lword_computes line 173
  48. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.lword_pack line 174
  49. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.Resources.tword_pack line 175