OAI/Computability/VertexCover/PCP/RepetitionUpper.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Soundness.RepetitionUpper.bernoulliAverage line 40
2. theorem OAI.UniqueGames.Soundness.RepetitionUpper.bernoulliAverage_scale line 46
3. theorem OAI.UniqueGames.Soundness.RepetitionUpper.bernoulliAverage_geometric line 54
4. theorem OAI.UniqueGames.Soundness.RepetitionUpper.bernoulliAverage_mono line 66
5. theorem OAI.UniqueGames.Soundness.RepetitionUpper.success_le_geometric line 81
6. theorem OAI.UniqueGames.Soundness.RepetitionUpper.pow_mono_nonneg line 92
7. def OAI.UniqueGames.Soundness.RepetitionUpper.zeroProbability line 104
8. theorem OAI.UniqueGames.Soundness.RepetitionUpper.zeroProbability_nonneg line 106
9. theorem OAI.UniqueGames.Soundness.RepetitionUpper.zeroProbability_le_one line 109
10. theorem OAI.UniqueGames.Soundness.RepetitionUpper.zeroProbability_antitone line 117
11. theorem OAI.UniqueGames.Soundness.RepetitionUpper.geometric_le_dimension_bound line 136
12. theorem OAI.UniqueGames.Soundness.RepetitionUpper.projection_upper_bound line 150
13. def OAI.UniqueGames.Soundness.RepetitionUpper.decoderThreshold line 161
14. theorem OAI.UniqueGames.Soundness.RepetitionUpper.decoderThreshold_pos line 163
15. theorem OAI.UniqueGames.Soundness.RepetitionUpper.exists_pos_nat_gt line 172
16. theorem OAI.UniqueGames.Soundness.RepetitionUpper.power_mul_growth_le_one line 181
17. theorem OAI.UniqueGames.Soundness.RepetitionUpper.exists_power_lt line 197
18. theorem OAI.UniqueGames.Soundness.RepetitionUpper.zeroProbability_pos line 214
19. theorem OAI.UniqueGames.Soundness.RepetitionUpper.exists_repetition_length line 217
20. theorem OAI.UniqueGames.Soundness.RepetitionUpper.soundness_of_bounds line 231
21. theorem OAI.UniqueGames.Soundness.RepetitionUpper.soundness_from_repetition line 246