OAI/Combinatorics/MatchingPSD/TypeProbabilities.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingSmoothing.pow_mul_factorial_le_mode line 9
  2. lemma OAI.MatchingSmoothing.poisson_mass_le_integer_mode line 31
  3. lemma OAI.MatchingSmoothing.multinomial_term_eq line 37
  4. lemma OAI.MatchingSmoothing.multinomial_term_le_mode line 48
  5. lemma OAI.MatchingSmoothing.card_piAntidiag_univ_le line 58
  6. lemma OAI.MatchingSmoothing.multinomial_mode_lower line 76
  7. def OAI.MatchingSmoothing.functionFiberEquiv line 99
  8. lemma OAI.MatchingSmoothing.card_functionFiber line 107
  9. lemma OAI.MatchingSmoothing.prod_eq_prod_histogram line 113
  10. lemma OAI.MatchingSmoothing.sum_product_of_types line 122
  11. lemma OAI.MatchingSmoothing.sum_product_of_type_probabilities line 139
  12. lemma OAI.MatchingSmoothing.sum_type_probability_eq_multinomial line 157
  13. lemma OAI.MatchingSmoothing.integer_mean_type_probability_lower line 176