OAI/Computability/VertexCover/Sampling/Basic.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.CorrelatedSampling.firstAccepted line 40
2. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.first_union_common line 45
3. def OAI.UniqueGames.Foundations.CorrelatedSampling.thresholdSample line 68
4. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.thresholdSample_agreement line 72
5. def OAI.UniqueGames.Foundations.CorrelatedSampling.totalVariation line 91
6. def OAI.UniqueGames.Foundations.CorrelatedSampling.overlapMass line 93
7. def OAI.UniqueGames.Foundations.CorrelatedSampling.unionMass line 95
8. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.totalVariation_nonneg line 97
9. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.overlapMass_nonneg line 101
10. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.min_abs_identity line 105
11. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.max_abs_identity line 112
12. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.overlapMass_eq line 119
13. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.unionMass_eq line 127
14. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.totalVariation_le_one line 135
15. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.overlap_union_ratio line 142
16. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.overlap_union_ratio_lower_bound line 148
17. theorem OAI.UniqueGames.Foundations.CorrelatedSampling.first_union_disagreement_upper_bound line 157