OAI/Combinatorics/BalancedRyser/Candidates/CandidateGlobalLineMean.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.CandidateGlobalLine.lineSuccessEvent line 16
2. theorem OAI.Balanced.CandidateGlobalLine.conditionalProbability_mono line 20
3. theorem OAI.Balanced.CandidateGlobalLine.lineSuccessEvent_probability_le line 29
4. theorem OAI.Balanced.CandidateGlobalLine.fresh_lineSuccessEvent_probability_le line 35
5. theorem OAI.Balanced.CandidateGlobalLine.one_old_lineSuccessEvent_probability_le line 52
6. theorem OAI.Balanced.CandidateGlobalLine.lineSuccess_sum_zero_one_le line 66
7. theorem OAI.Balanced.CandidateGlobalLine.sum_targets_lineSuccess_zero_one_le line 91