OAI/Combinatorics/BalancedRyser/Probability/HypergeometricApproximation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.abs_prod_sub_prod_le_sum_errors line 11
  2. theorem OAI.Balanced.descFactorial_factor_error line 41
  3. theorem OAI.Balanced.descFactorial_ratio_power_error line 77
  4. theorem OAI.Balanced.descFactorial_ratio_power_error_uniform line 112
  5. theorem OAI.Balanced.tendsto_descFactorial_ratio_sub_power line 132
  6. theorem OAI.Balanced.tendsto_descFactorial_ratio line 147
  7. theorem OAI.Balanced.choose_ratio_eq_descFactorial_ratio line 156
  8. theorem OAI.Balanced.uniform_subset_contains_probability line 172
  9. theorem OAI.Balanced.uniform_subset_contains_probability_error line 192
  10. theorem OAI.Balanced.uniform_subset_after_target_probability line 201