OAI/Combinatorics/BalancedRyser/Profiles/ProfileScheduledMargin.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.ProfileScheduledMargin.threshold line 17
2. theorem OAI.Balanced.ProfileScheduledMargin.threshold_pos line 19
3. theorem OAI.Balanced.ProfileScheduledMargin.threshold_antitone line 21
4. def OAI.Balanced.ProfileScheduledMargin.sourceTest line 26
5. theorem OAI.Balanced.ProfileScheduledMargin.sourceTest_mono line 29
6. theorem OAI.Balanced.ProfileScheduledMargin.exists_source_mean_margin line 34
7. def OAI.Balanced.ProfileScheduledMargin.tailProbability line 55
8. theorem OAI.Balanced.ProfileScheduledMargin.tailProbability_ge line 60
9. theorem OAI.Balanced.ProfileScheduledMargin.exists_uniform_positive_tail line 93