OAI/NumberTheory/Jacobsthal/Estimates/ActualCollisionBound.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosInverseAlignment.sourceRationalList line 14
  2. theorem OAI.Erdos970.ErdosInverseAlignment.mem_sourceRationalList line 17
  3. theorem OAI.Erdos970.ErdosInverseAlignment.source_height_product_bound line 26
  4. theorem OAI.Erdos970.ErdosInverseAlignment.source_rational_list_bound line 36
  5. theorem OAI.Erdos970.ErdosPrimitiveIntercept.InterceptReduction.denominator_le line 53
  6. theorem OAI.Erdos970.ErdosPrimitiveIntercept.InterceptReduction.numerator_abs_le line 58
  7. theorem OAI.Erdos970.ErdosPrimitiveIntercept.InterceptReduction.height_transfer line 63
  8. theorem OAI.Erdos970.ErdosPrimitiveIntercept.exists_canonical_structured_intercept line 79
  9. def OAI.Erdos970.ErdosInverseStructured.Structured line 98
  10. def OAI.Erdos970.ErdosInverseStructured.Nonstructured line 102
  11. theorem OAI.Erdos970.ErdosInverseStructured.structured_of_line_alignment line 105
  12. theorem OAI.Erdos970.ErdosInverseStructured.nonstructured_not_aligned_on_line line 116
  13. def OAI.Erdos970.ErdosLineCollision.slopeClass line 131
  14. theorem OAI.Erdos970.ErdosLineCollision.unaligned_numerator_ne_zero line 136
  15. theorem OAI.Erdos970.ErdosLineCollision.point_residue_eq_slopeClass line 152
  16. def OAI.Erdos970.ErdosLineCollision.incidentPoints line 180
  17. def OAI.Erdos970.ErdosLineCollision.occupiedClasses line 185
  18. theorem OAI.Erdos970.ErdosLineCollision.occupiedClasses_subset_slope_image line 189
  19. theorem OAI.Erdos970.ErdosLineCollision.occupiedClasses_card_le line 200
  20. def OAI.Erdos970.ErdosLineCollision.occupiedRows line 215
  21. def OAI.Erdos970.ErdosLineCollision.RowIncidence line 220
  22. theorem OAI.Erdos970.ErdosLineCollision.row_modulus_mem line 224
  23. theorem OAI.Erdos970.ErdosLineCollision.point_rows_eq line 232
  24. theorem OAI.Erdos970.ErdosLineCollision.point_rows_card line 252
  25. theorem OAI.Erdos970.ErdosLineCollision.occupiedRows_card_le line 270
  26. def OAI.Erdos970.ErdosLineCollision.commonRows line 281
  27. theorem OAI.Erdos970.ErdosLineCollision.commonRows_modulus_injective line 285
  28. theorem OAI.Erdos970.ErdosLineCollision.commonRows_modulus_divides line 294
  29. theorem OAI.Erdos970.ErdosLineCollision.commonRows_card_le line 306
  30. theorem OAI.Erdos970.ErdosLineCollision.row_multiplicity_sum line 331
  31. theorem OAI.Erdos970.ErdosLineCollision.total_incidence_le_product line 361
  32. theorem OAI.Erdos970.ErdosLineCollision.actual_collision_bound line 376