OAI/Combinatorics/BalancedRyser/Probability/PatternWeights.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.PatternMoments.weightMeasure line 13
2. lemma OAI.Balanced.PatternMoments.weightMeasure_univ line 16
3. lemma OAI.Balanced.PatternMoments.isProbabilityMeasure_weightMeasure line 21
4. lemma OAI.Balanced.PatternMoments.weightMeasure_real_singleton line 27
5. lemma OAI.Balanced.PatternMoments.integral_weightMeasure_eq_expectation line 33
6. theorem OAI.Balanced.PatternMoments.expectation_centered_pattern_prod_eq_zero line 43
7. theorem OAI.Balanced.PatternMoments.abs_expectation_le line 63
8. theorem OAI.Balanced.PatternMoments.abs_centered_prod_le line 73
9. theorem OAI.Balanced.PatternMoments.abs_expectation_centered_prod_le line 88