OAI/Computability/VertexCover/Sampling/SharedProfiles.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.CorrelatedSampling.profileThresholds line 45
2. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.mem_profileThresholds line 50
3. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.distribution_weight_le_one line 55
4. def OAI.UniqueGames.Foundations.CorrelatedSampling.sharedProfileThresholds line 64
5. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.left_mem_sharedProfileThresholds line 68
6. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.right_mem_sharedProfileThresholds line 73
7. abbrev OAI.UniqueGames.Foundations.CorrelatedSampling.SharedProfileSeed line 78
8. def OAI.UniqueGames.Foundations.CorrelatedSampling.sharedProfileLeft line 82
9. def OAI.UniqueGames.Foundations.CorrelatedSampling.sharedProfileRight line 86
10. def OAI.UniqueGames.Foundations.CorrelatedSampling.sharedProfileReject line 90
11. def OAI.UniqueGames.Foundations.CorrelatedSampling.uniformRejectionRate line 95
12. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.uniformRejectionRate_nonnegative line 98
13. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.uniformRejectionRate_lt_one line 107
14. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.sharedProfileReject_nonnegative line 115
15. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.sharedProfile_reject_le_rate line 121
16. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.nonnegative_powers_mono line 153
17. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.sharedProfile_label_diagonal_bound line 162
18. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.exists_uniformRejectionRate_pow_lt line 196