OAI/Combinatorics/KMedianRecovery/Branching/BranchPhysical.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.plan_pack line 18
  2. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.completion_pack line 39
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchProgram.run_pack line 48
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.Ready line 66
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.outside line 70
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.outside_computes line 71
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.badBall line 73
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.badBall_computes line 74
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.badBalls line 75
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.badBalls_computes line 76
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.badRadius line 78
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.badRadius_computes line 79
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.badRadii line 81
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.badRadii_computes line 82
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.lhs line 84
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.lhs_computes line 85
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.rhs line 89
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.rhs_computes line 91
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.run line 95
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.run_computes line 97
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.outside_pack line 106
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.badBalls_pack line 109
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.badRadii_pack line 113
  24. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.lhs_pack line 117
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.rhs_pack line 120