OAI/Combinatorics/KMedianRecovery/Algorithms/GlobalOuterProbability.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.run_take line 10
2. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.probability_all line 14
3. theorem OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.finite_program line 18
4. def OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.algorithm line 97
5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.algorithm_output line 105
6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.probability_eq line 110
7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.expected_eq line 117
8. theorem OAI.MetricKMedianRecovery.BitMachine.BinaryGlobalOuter.algorithm_guarantee line 121