OAI/Computability/PerfectCompleteness/Decoding/DependentDecoderSampling.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PerfectCompleteness.DependentDecoderSampling.Seed line 21
2. def OAI.PerfectCompleteness.DependentDecoderSampling.seedLaw line 24
3. theorem OAI.PerfectCompleteness.DependentDecoderSampling.read_law line 29
4. def OAI.PerfectCompleteness.DependentDecoderSampling.sampleLaw line 40
5. theorem OAI.PerfectCompleteness.DependentDecoderSampling.sample_probability_eq line 46
6. theorem OAI.PerfectCompleteness.DependentDecoderSampling.probability_le_of_supported_seeds line 76
7. theorem OAI.PerfectCompleteness.DependentDecoderSampling.supported_left line 88
8. theorem OAI.PerfectCompleteness.DependentDecoderSampling.supported_right line 100