OAI/Computability/VertexCover/Sampling/TraceLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.CorrelatedSampling.traceAverage line 46
2. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.traceAverage_const line 50
3. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.traceAverage_mono line 56
4. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.traceAverage_sum line 68
5. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.firstAccepted_law line 80
6. def OAI.UniqueGames.Foundations.CorrelatedSampling.goodFirstIndicator line 126
7. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.goodFirstIndicator_expansion line 131
8. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.goodFirstIndicator_law line 147