OAI/Computability/PerfectCompleteness/Decoding/FixedDecoderCleanRateLemmas.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PerfectCompleteness.FixedDecoderCleanRate.F2 line 16
2. structure OAI.PerfectCompleteness.FixedDecoderCleanRate.Geometry line 18
3. def OAI.PerfectCompleteness.FixedDecoderCleanRate.setup line 35
4. theorem OAI.PerfectCompleteness.FixedDecoderCleanRate.calls_le line 48
5. theorem OAI.PerfectCompleteness.FixedDecoderCleanRate.cubePositive line 56
6. theorem OAI.PerfectCompleteness.FixedDecoderCleanRate.branchPositive line 60
7. theorem OAI.PerfectCompleteness.FixedDecoderCleanRate.probability_lt_accuracy line 77
8. abbrev OAI.PerfectCompleteness.FixedDecoderPairRate.F2 line 103
9. theorem OAI.PerfectCompleteness.FixedDecoderPairRate.probability_lt_accuracy line 123