OAI/Combinatorics/KMedianRecovery/Recovery/FinishPhase.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.RationalPhase.finish_phase line 10
  2. lemma OAI.MetricKMedianRecovery.RationalPhase.run_phase line 18
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.powerInput line 30
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.powerInput_computes line 32
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.dummy line 40
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.powerInput_pack line 41
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.power line 46
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.power_computes line 48
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.phase_field line 51
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.power_pack line 55
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.cf line 59
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.cf_computes line 60
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.contextAt line 61
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.contextAt_computes line 63
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.contextAt_pack line 70
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.zeroBudget line 75
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.zeroBudget_computes line 77
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.zeroBudget_pack line 79
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.start line 86
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.start_computes line 88
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.start_pack line 89
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.included line 94
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.included_computes line 95
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.regularOpened line 97
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.regularOpened_computes line 99
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.regularOpened_pack line 102
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.prepare line 121
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.prepare_computes line 123
  29. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.prepare_pack line 126
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.run line 132
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.run_computes line 134
  32. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseCount.run_pack line 137