OAI/Combinatorics/BalancedRyser/Candidates/CandidateHighMoments.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.CandidateExposure.rootPatternModel_total_le line 15
2. theorem OAI.Balanced.CandidateExposure.rootPatternModel_overlap_le line 21
3. def OAI.Balanced.CandidateExposure.centeredMomentConstant line 28
4. theorem OAI.Balanced.CandidateExposure.centeredMomentConstant_nonneg line 32
5. theorem OAI.Balanced.CandidateExposure.rootPatternModel_centered_moment_le line 36
6. theorem OAI.Balanced.CandidateExposure.conditional_successfulTupleCount_centered_moment_le line 61
7. theorem OAI.Balanced.CandidateExposure.successfulTupleCount_centered_moment_le line 72