OAI/NumberTheory/Jacobsthal/Estimates/SourcePairRemainder.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.ErdosHyperbolaError.source_restriction_divides line 17
  2. theorem OAI.Erdos970.ErdosHyperbolaError.source_dilation_coprime line 31
  3. theorem OAI.Erdos970.ErdosHyperbolaError.source_product_coprime line 37
  4. theorem OAI.Erdos970.ErdosHyperbolaError.source_totient_product line 53
  5. def OAI.Erdos970.ErdosHyperbolaError.reducedProduct line 73
  6. def OAI.Erdos970.ErdosHyperbolaError.reducedClass line 76
  7. def OAI.Erdos970.ErdosHyperbolaError.dilatedPairs line 80
  8. theorem OAI.Erdos970.ErdosHyperbolaError.mem_dilatePair_iff line 84
  9. theorem OAI.Erdos970.ErdosHyperbolaError.reduced_pairs_image line 104
  10. theorem OAI.Erdos970.ErdosHyperbolaError.dilatedPairs_card line 121
  11. def OAI.Erdos970.ErdosHyperbolaError.realIntervalIntegers line 140
  12. def OAI.Erdos970.ErdosHyperbolaError.sourcePairs line 145
  13. def OAI.Erdos970.ErdosHyperbolaError.sourceInterval line 152
  14. theorem OAI.Erdos970.ErdosHyperbolaError.sourceInterval_points line 161
  15. theorem OAI.Erdos970.ErdosHyperbolaError.sourcePairs_eq_dilated line 168
  16. def OAI.Erdos970.ErdosHyperbolaError.zeroDensity line 198
  17. def OAI.Erdos970.ErdosHyperbolaError.mainDensity line 202
  18. theorem OAI.Erdos970.ErdosHyperbolaError.count_minus_zero_density line 207
  19. theorem OAI.Erdos970.ErdosHyperbolaError.count_spectral_error line 225
  20. theorem OAI.Erdos970.ErdosHyperbolaError.count_error_base line 241
  21. theorem OAI.Erdos970.ErdosHyperbolaError.mainDensity_explicit line 263
  22. def OAI.Erdos970.ErdosHyperbolaError.completionConstant line 272
  23. theorem OAI.Erdos970.ErdosHyperbolaError.completionConstant_pos line 274
  24. theorem OAI.Erdos970.ErdosHyperbolaError.hyperbola_count_error line 279
  25. theorem OAI.Erdos970.ErdosHyperbolaError.dilated_hyperbola_count_error line 304
  26. theorem OAI.Erdos970.ErdosHyperbolaError.dilated_hyperbola_count_error_same_step line 341
  27. theorem OAI.Erdos970.ErdosHyperbolaError.source_hyperbola_count_error line 368
  28. theorem OAI.Erdos970.ErdosVarianceLargeCount.signed_squarefree_dvd_iff line 404
  29. theorem OAI.Erdos970.ErdosVarianceLargeCount.sourcePairs_divisor_filter line 409
  30. theorem OAI.Erdos970.ErdosVarianceLargeCount.sourcePairs_intersection_mass line 419
  31. def OAI.Erdos970.ErdosVarianceLargeCount.sourceMain line 444
  32. def OAI.Erdos970.ErdosVarianceLargeCount.hyperbolaEnvelope line 448
  33. theorem OAI.Erdos970.ErdosVarianceLargeCount.source_pair_remainder_bound line 452