OAI/Combinatorics/BalancedRyser/Profiles/ProfileHypergeometric.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.weighted_profile_error_of_mean_bound line 8
2. theorem OAI.Balanced.descFactorial_ratio_bounds line 53
3. theorem OAI.Balanced.abs_mul_sub_mul_le_errors line 63
4. theorem OAI.Balanced.two_descFactorial_factors_error line 73
5. theorem OAI.Balanced.weighted_two_descFactorial_factors_error line 90
6. theorem OAI.Balanced.exists_profile_approximation_cutoff line 122
7. theorem OAI.Balanced.uniform_weighted_hypergeometric_approximation line 149