OAI/Combinatorics/BalancedRyser/Probability/PatternConditionalMean.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.PatternModel.measurable_fixCoordinates_joint line 12
2. theorem OAI.Balanced.PatternModel.measurable_fixedExpectation line 25
3. theorem OAI.Balanced.PatternModel.fixedExpectation_eq_of_agree line 31
4. theorem OAI.Balanced.PatternModel.fixedExpectation_fixCoordinates line 41
5. theorem OAI.Balanced.PatternTails.allowed_count_tail_le line 54
6. theorem OAI.Balanced.PatternTails.allowed_centered_count_tail_le line 68