OAI/Combinatorics/BalancedRyser/Probability/UniformKernel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.UniformKernel.fiberMass line 13
2. theorem OAI.Balanced.UniformKernel.fiberMass_le line 16
3. theorem OAI.Balanced.UniformKernel.fiberMass_nonneg line 35
4. theorem OAI.Balanced.UniformKernel.assignmentMass_le line 41
5. theorem OAI.Balanced.UniformKernel.conditional_assignmentMass_le line 52
6. theorem OAI.Balanced.UniformKernel.offsetAverage_le line 75
7. theorem OAI.Balanced.UniformKernel.totalMass_le_one line 85