OAI/Combinatorics/BalancedRyser/Probability/FiniteCenteredPatternLemmas.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.PatternModel.centered_moment_le_of_exposureBounds line 16
2. theorem OAI.Balanced.PatternModel.overlapCount_le_allExposed line 56
3. theorem OAI.Balanced.PatternModel.integrable_fixed_overlapCount line 74
4. theorem OAI.Balanced.PatternModel.centered_moment_le_of_allExposedBounds line 86
5. theorem OAI.Balanced.uniformCenteredPatternMoments_of_exposureBounds line 122
6. theorem OAI.Balanced.patternMoments_proof line 157