OAI/Combinatorics/KMedianRecovery/Branching/BranchSeedLayout.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.completionCount line 9
  2. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.colorCount line 12
  3. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.labelCount line 13
  4. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.count line 14
  5. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Seed line 15
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.split line 16
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.colors line 18
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.labels line 20
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.layout line 22
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.colorTensor line 27
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.labelTensor line 28
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.raw line 30
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.colorTensor_colors line 33
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.labelTensor_labels line 37
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.raw_colors line 41
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.raw_labels line 45
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.split_raw line 49
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.raw_layout line 53
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.probability_layout line 58
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.nword line 67
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.nword_computes line 68
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.mword line 69
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.mword_computes line 70
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.blog line 71
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.blog_computes line 72
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.cshape line 73
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.cshape_computes line 74
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.lshape line 75
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.lshape_computes line 76
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.csize line 77
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.csize_computes line 78
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.lsize line 81
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.lsize_computes line 83
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.craw line 86
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.craw_computes line 87
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.rest line 89
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.rest_computes line 90
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.lraw line 92
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.lraw_computes line 93
  40. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.tailBits line 95
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.tailBits_computes line 96
  42. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.colors line 98
  43. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.colors_computes line 99
  44. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.labels line 101
  45. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.labels_computes line 103
  46. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.context line 106
  47. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.context_computes line 110
  48. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.nword_pack line 116
  49. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.mword_pack line 118
  50. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.blog_pack line 121
  51. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.csize_pack line 124
  52. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.lsize_pack line 126
  53. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.cshape_pack line 129
  54. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.lshape_pack line 130
  55. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.craw_pack line 133
  56. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.rest_pack line 138
  57. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.lraw_pack line 145
  58. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.tailBits_pack line 150
  59. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.colors_pack line 157
  60. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.labels_pack line 161
  61. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRandomize.context_pack line 172