OAI/Combinatorics/KMedianRecovery/Branching/BranchContext.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.pack line 10
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.remaining line 15
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.remaining_computes line 16
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.context line 19
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.context_computes line 20
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.oracle line 23
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.oracle_computes line 24
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.classOf line 27
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.classOf_computes line 29
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.greenContext line 32
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.greenContext_computes line 33
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.greenOracle line 36
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.greenOracle_computes line 37
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.ballInput line 40
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.ballInput_computes line 41
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.copyData line 44
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.copyData_computes line 45
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.parts line 48
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.parts_computes line 49
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.origins line 52
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.origins_computes line 53
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.locations line 58
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.locations_computes line 59
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.balls line 62
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.remaining_pack line 70
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.context_pack line 73
  27. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.oracle_pack line 78
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.classOf_pack line 81
  29. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.greenContext_pack line 85
  30. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.greenOracle_pack line 92
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.leavesBits_eq line 95
  32. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.ballInput_pack line 100
  33. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.copyData_pack line 104
  34. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.parts_pack line 107
  35. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.origins_pack line 109
  36. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchContext.locations_pack line 111