OAI/Combinatorics/KMedianRecovery/Geometry/LocalRefineMachine.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.LocalSearch.executableRefineFuel_spec line 8
2. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalRefine.run line 27
3. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalRefine.run_computes line 29
4. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalRefine.pack line 31
5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalRefine.run_pack line 33
6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalRefine.fuel_bound line 44
7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalRefine.integral_spec line 57