OAI/NumberTheory/PiExponent/Analysis/CollisionCombinatorics.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponent.Collision.choose_card_le_sum line 9
  2. theorem OAI.PiExponent.Collision.choose_card_le_sum_of_injOn line 27
  3. def OAI.PiExponent.Collision.multiplicity line 34
  4. theorem OAI.PiExponent.Collision.sum_multiplicity line 38
  5. theorem OAI.PiExponent.Collision.sum_choose_multiplicity_le_sum_degree line 45
  6. theorem OAI.PiExponent.Collision.sum_choose_multiplicity_le_sum_degree_univ line 65
  7. theorem OAI.PiExponent.Collision.sum_multiplicity_univ line 73
  8. theorem OAI.PiExponent.Collision.sum_sq_multiplicity_sub_card_le_twice_sum_degree line 79
  9. theorem OAI.PiExponent.Collision.sum_sq_multiplicity_sub_card_le_twice_sum_degree_univ line 104
  10. theorem OAI.PiExponent.Collision.sum_multiplicity_eq_card_filter line 113
  11. theorem OAI.PiExponent.Collision.cutoff_mul_high_count_le_sum line 119
  12. theorem OAI.PiExponent.Collision.sum_weight_ge_of_low_count_le line 137