OAI/Combinatorics/BalancedRyser/Probability/PatternExposureIdentities.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.PatternExposure.measurable_fixedExpectation line 14
2. theorem OAI.Balanced.PatternExposure.ofReal_fixedExpectation_eq_lmarginal line 30
3. theorem OAI.Balanced.PatternExposure.fixedExpectation_tower_of_nonneg_bounded line 40
4. theorem OAI.Balanced.PatternExposure.fixedExpectation_count_tower line 71
5. theorem OAI.Balanced.PatternExposure.indicator_fixed_of_support_subset line 87
6. theorem OAI.Balanced.PatternExposure.count_fixed_of_support_subset line 94
7. theorem OAI.Balanced.PatternExposure.fixedExpectation_count_of_support_subset line 102
8. theorem OAI.Balanced.PatternExposure.centeredMoment_zero_of_support_subset line 109