OAI/Combinatorics/KMedianRecovery/Branching/BranchPrefix.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.BinaryRandomizedBranch.Prefix.run line 9
2. def OAI.MetricKMedianRecovery.BitMachine.BinaryRandomizedBranch.Prefix.run_computes line 10
3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRandomizedBranch.Prefix.source_run line 12
4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRandomizedBranch.Prefix.probability_layout line 27
5. def OAI.MetricKMedianRecovery.BitMachine.BinaryRandomizedZeroBranch.Prefix.run line 36
6. def OAI.MetricKMedianRecovery.BitMachine.BinaryRandomizedZeroBranch.Prefix.run_computes line 37
7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRandomizedZeroBranch.Prefix.run_pack line 39
8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRandomizedZeroBranch.Prefix.probability_layout line 50