OAI/Combinatorics/KMedianRecovery/Recovery/Min.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.RatOps.min line 9
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.sf line 19
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.sf_computes line 20
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.paramV line 21
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.paramZ line 22
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.paramV_computes line 23
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.paramZ_computes line 24
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.phase line 25
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.phase_computes line 26
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.parameters_pack line 28
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.query line 35
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.query_computes line 36
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.activityInput_pack line 37
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.isActive line 45
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.isActive_computes line 46
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.isActive_pack line 47
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.nearest line 52
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.nearest_computes line 54
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.nearest_pack line 59
  20. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.opened_nil line 63
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.clippedItem line 73
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.clippedItem_computes line 76
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.clippedItem_pack line 91
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.budgetItem line 97
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.budgetItem_computes line 100
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.budgetItem_pack line 102
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.budget line 109
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.budget_computes line 111
  29. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.budget_pack line 117
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.context line 126
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.context_computes line 128
  32. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.context_pack line 132
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.run line 138
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.run_computes line 139
  35. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseAdvance.run_pack line 140