OAI/Combinatorics/KMedianRecovery/Machines/RecoveryTape.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.tapeSize line 14
2. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.positiveSeed line 15
3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.zeroCount_bound line 19
4. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.zeroSeed line 23
5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.atBranch_context line 26
6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.atBranch_source line 35
7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.atZero_context line 54
8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.atZero_pack line 65
9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.positiveSeed_probability line 74
10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.zeroSeed_probability line 78