OAI/NumberTheory/Jacobsthal/Estimates/PairCollisionCount.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosKloosterman.sum line 23
  2. def OAI.Erdos970.ErdosKloosterman.standardSum line 27
  3. theorem OAI.Erdos970.ErdosKloosterman.sum_swap line 30
  4. theorem OAI.Erdos970.ErdosKloosterman.sum_unit_scale line 35
  5. theorem OAI.Erdos970.ErdosKloosterman.sum_ringEquiv line 43
  6. theorem OAI.Erdos970.ErdosKloosterman.sum_zero_zero line 50
  7. theorem OAI.Erdos970.ErdosKloosterman.standardSum_exp line 53
  8. def OAI.Erdos970.ErdosHyperbolaIdentities.integerWeight line 79
  9. def OAI.Erdos970.ErdosHyperbolaIdentities.unitClass line 82
  10. def OAI.Erdos970.ErdosHyperbolaIdentities.restrictedSum line 86
  11. def OAI.Erdos970.ErdosHyperbolaIdentities.hyperbolaPairs line 91
  12. def OAI.Erdos970.ErdosHyperbolaIdentities.integerFibre line 97
  13. def OAI.Erdos970.ErdosHyperbolaIdentities.pairFibre line 100
  14. theorem OAI.Erdos970.ErdosHyperbolaIdentities.mem_unitClass line 105
  15. theorem OAI.Erdos970.ErdosHyperbolaIdentities.mem_integerFibre line 109
  16. theorem OAI.Erdos970.ErdosHyperbolaIdentities.unit_class_of_int line 112
  17. def OAI.Erdos970.ErdosKloosterman.productChar line 131
  18. theorem OAI.Erdos970.ErdosKloosterman.sum_product line 139
  19. theorem OAI.Erdos970.ErdosKloosterman.sum_product_ringEquiv line 162
  20. theorem OAI.Erdos970.ErdosKloosterman.PrimePower.shift_mul_inverse line 179
  21. def OAI.Erdos970.ErdosKloosterman.PrimePower.shiftUnit line 186
  22. theorem OAI.Erdos970.ErdosKloosterman.PrimePower.shiftUnit_val line 190
  23. theorem OAI.Erdos970.ErdosKloosterman.PrimePower.shiftUnit_inv_val line 193
  24. def OAI.Erdos970.ErdosKloosterman.PrimePower.shiftEquiv line 196
  25. theorem OAI.Erdos970.ErdosKloosterman.PrimePower.phase_shift line 202
  26. theorem OAI.Erdos970.ErdosKloosterman.pair_eq_or_swap line 220
  27. theorem OAI.Erdos970.ErdosKloosterman.inverse_pair_collision line 233
  28. theorem OAI.Erdos970.ErdosHyperbolaIdentities.card_mul_fibre line 264
  29. theorem OAI.Erdos970.ErdosHyperbolaIdentities.unitClass_card_mul_totient line 278
  30. theorem OAI.Erdos970.ErdosHyperbolaIdentities.restrictedSum_zero line 285
  31. theorem OAI.Erdos970.ErdosHyperbolaIdentities.restrictedSum_zero_eq_totient_ratio line 290
  32. def OAI.Erdos970.ErdosKloosterman.pairCollisions line 316
  33. theorem OAI.Erdos970.ErdosKloosterman.pairCollisions_card_le line 321