OAI/Combinatorics/BalancedRyser/Probability/PatternExtension.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Balanced.PatternMoments.expectation_add line 11
2. lemma OAI.Balanced.PatternMoments.expectation_nonneg line 15
3. theorem OAI.Balanced.PatternMoments.positive_extension_sum line 19
4. theorem OAI.Balanced.PatternMoments.centered_weight_extension_bound line 33
5. def OAI.Balanced.PatternMoments.positiveWeight line 53
6. lemma OAI.Balanced.PatternMoments.positiveWeight_nil line 57
7. lemma OAI.Balanced.PatternMoments.positiveWeight_nonneg line 62
8. lemma OAI.Balanced.PatternMoments.positiveWeight_perm line 73
9. theorem OAI.Balanced.PatternMoments.positiveWeight_extension line 81
10. theorem OAI.Balanced.PatternMoments.centered_weight_extension_bound_finset line 100