OAI/Combinatorics/BalancedRyser/Probability/PatternModelCancellation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.PatternProof.fillFresh line 13
2. lemma OAI.Balanced.PatternProof.measurable_fillFresh line 18
3. lemma OAI.Balanced.PatternProof.measurable_indicator line 27
4. lemma OAI.Balanced.PatternProof.indicator_mem_Icc line 30
5. lemma OAI.Balanced.PatternProof.indicator_fillFresh_eq_fixed line 35
6. theorem OAI.Balanced.PatternProof.fixedExpectation_centered_prod_eq_zero line 46
7. lemma OAI.Balanced.PatternProof.measurable_fixedCoordinates line 76
8. lemma OAI.Balanced.PatternProof.fixedExpectation_indicator_mem_Icc line 85
9. theorem OAI.Balanced.PatternProof.abs_fixedExpectation_centered_prod_le line 101