OAI/Combinatorics/KMedianRecovery/Recovery/Fuel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.fuel line 9
2. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.fuel_computes line 10
3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.fuel_pack line 11
4. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.completed line 16
5. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.completed_computes line 17
6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.completed_pack line 18
7. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.step line 22
8. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.step_computes line 23
9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.step_pack line 24
10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseRun.iterate_pack line 28
11. lemma OAI.MetricKMedianRecovery.RationalHeight.Height.min line 36