OAI/Combinatorics/IndependentSets/Repetition/Basic2.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.firstAccepted line 7
2. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.first_union_common line 12
3. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.thresholdSample line 35
4. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.thresholdSample_agreement line 39
5. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.totalVariation line 58
6. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.overlapMass line 60
7. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.unionMass line 62
8. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.totalVariation_nonneg line 64
9. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.overlapMass_nonneg line 68
10. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.min_abs_identity line 72
11. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.max_abs_identity line 79
12. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.overlapMass_eq line 86
13. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.unionMass_eq line 94
14. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.totalVariation_le_one line 102
15. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.overlap_union_ratio line 109
16. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.overlap_union_ratio_lower_bound line 115
17. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.first_union_disagreement_upper_bound line 124