OAI/Combinatorics/BalancedRyser/Profiles/PoissonProfile.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.PoissonProfile.eq_pow_div_factorial_mul_zero line 10
  2. theorem OAI.Balanced.PoissonProfile.factorization line 28
  3. theorem OAI.Balanced.PoissonProfile.column_hasSum line 34
  4. theorem OAI.Balanced.PoissonProfile.factorization_marginal line 41
  5. theorem OAI.Balanced.PoissonProfile.weighted_total_eq_exp_mul_row line 52
  6. theorem OAI.Balanced.PoissonProfile.weighted_row_eq_exp_neg_mul_total line 71
  7. theorem OAI.Balanced.PoissonProfile.first_moment_row line 78
  8. theorem OAI.Balanced.PoissonProfile.row_rigidity line 84
  9. theorem OAI.Balanced.PoissonProfile.column_zero_of_first_zero line 112
  10. theorem OAI.Balanced.PoissonProfile.supported_on_one line 118
  11. theorem OAI.Balanced.PoissonProfile.no_uncovered_mass line 128