OAI/Combinatorics/KMedianRecovery/Algorithms/IntegralRecoverySemantics.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.stateAt line 10
2. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.stateAt_bounded line 16
3. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.optionOutput line 24
4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.optionOutput_none line 29
5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.optionOutput_some line 32
6. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.candidates line 37
7. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.result line 41
8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.run_source line 45