OAI/Combinatorics/KMedianRecovery/Branching/RandomizedZeroBranch.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryRandomizedZeroBranch.run line 9
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryRandomizedZeroBranch.run_computes line 11
  3. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryRandomizedZeroBranch.Seed line 13
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryRandomizedZeroBranch.embed line 14
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryRandomizedZeroBranch.raw line 15
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRandomizedZeroBranch.run_pack line 16
  7. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryRandomizedZeroBranch.count line 28
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryRandomizedZeroBranch.layout line 29
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRandomizedZeroBranch.raw_eq line 32
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRandomizedZeroBranch.raw_layout line 42
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.pword line 53
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.pword_computes line 54
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.qword line 55
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.qword_computes line 56
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.dimensions line 57
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.dimensions_computes line 58
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.tword line 60
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.lword line 61
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.bword line 62
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.tword_computes line 63
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.lword_computes line 64
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.bword_computes line 65
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.leftShape line 66
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.rightShape line 67
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.leftShape_computes line 68
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.rightShape_computes line 70
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.run line 72
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.run_computes line 75
  29. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.pword_pack line 83
  30. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.qword_pack line 86
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.dimensions_pack line 88
  32. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.leftShape_pack line 90
  33. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.rightShape_pack line 94
  34. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.run_pack line 96
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.cut line 105
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.cut_computes line 108
  37. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchTape.Count.cut_pack line 110