OAI/NumberTheory/PiExponent/Analysis/CollisionOccupancy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponent.Collision.sum_sq_le_card_mul_sum_sq line 11
  2. theorem OAI.PiExponent.Collision.sum_sq_le_card_mul_total_sq line 15
  3. theorem OAI.PiExponent.Collision.mass_sq_div_card_le_total_sq line 22
  4. theorem OAI.PiExponent.Collision.fraction_sq_mul_mass_sq_div_card_le_total_sq line 36
  5. theorem OAI.PiExponent.Collision.sum_sq_le_card_mul_univ_sq line 46
  6. theorem OAI.PiExponent.Collision.nat_occupancy_square_lower_bound line 50