OAI/Combinatorics/BalancedRyser/Profiles/ProfileClassMargin.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Balanced.ProfileClassMargin.Test line 18
2. def OAI.Balanced.ProfileClassMargin.cutoffMass line 21
3. def OAI.Balanced.ProfileClassMargin.LimitLowerBound line 27
4. structure OAI.Balanced.ProfileClassMargin.Object line 37
5. instance OAI.Balanced.ProfileClassMargin.(instance at line 46) line 46
6. instance OAI.Balanced.ProfileClassMargin.(instance at line 47) line 47
7. instance OAI.Balanced.ProfileClassMargin.(instance at line 48) line 48
8. theorem OAI.Balanced.ProfileClassMargin.exists_uniform_margin line 50
9. theorem OAI.Balanced.ProfileClassMargin.exists_uniform_count_margin line 108