OAI/Combinatorics/KMedianRecovery/Recovery/RefineMath.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.CanonicalMergeRefinement.adjacent line 8
  2. lemma OAI.MetricKMedianRecovery.CanonicalMergeRefinement.cuts_adjacent line 11
  3. def OAI.MetricKMedianRecovery.CanonicalMergeRefinement.refinedEdge line 21
  4. lemma OAI.MetricKMedianRecovery.CanonicalMergeRefinement.refinePath_adjacent line 25
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.spareWord line 40
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.spareWord_computes line 41
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.ct line 45
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.ct_computes line 46
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.ctSpare line 47
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.ctSpare_computes line 48
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.grown line 49
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.grown_computes line 50
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.removeOut line 55
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.removeOut_computes line 56
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.expand line 58
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.expand_computes line 59
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryJump.expand_pack line 61
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.edgeG line 81
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.edgeG_computes line 82
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.edgeView line 83
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.edgeView_computes line 84
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.edgeData line 85
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.edgeData_computes line 86
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.edge line 92
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryJump.edge_computes line 94
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryJump.edge_pack line 99