OAI/NumberTheory/Jacobsthal/Sieve/RealCoprimeResidueCount.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosInverseCRT.crtResidues line 15
  2. theorem OAI.Erdos970.ErdosInverseCRT.mem_crtResidues line 20
  3. theorem OAI.Erdos970.ErdosInverseCRT.crtResidues_card line 36
  4. theorem OAI.Erdos970.ErdosInverseCRT.intCast_mem_crtResidues line 41
  5. def OAI.Erdos970.Erdos66Dependency.SingleResidueCount.residueClass line 59
  6. theorem OAI.Erdos970.Erdos66Dependency.SingleResidueCount.count_exact line 62
  7. lemma OAI.Erdos970.Erdos66Dependency.SingleResidueCount.count_error_rat line 67
  8. theorem OAI.Erdos970.Erdos66Dependency.SingleResidueCount.count_error_length line 86
  9. theorem OAI.Erdos970.Erdos66Dependency.SingleResidueCount.count_error line 93
  10. theorem OAI.Erdos970.ErdosVarianceMoments.crt_coordinate_val line 113
  11. theorem OAI.Erdos970.ErdosVarianceMoments.literal_residue_choices_card line 125
  12. theorem OAI.Erdos970.ErdosVarianceMoments.canonical_filter_card line 137
  13. def OAI.Erdos970.ErdosVarianceMoments.allowedClasses line 152
  14. theorem OAI.Erdos970.ErdosVarianceMoments.mem_allowedClasses line 156
  15. theorem OAI.Erdos970.ErdosVarianceMoments.allowedClasses_card line 162
  16. def OAI.Erdos970.ErdosInverseCRT.integerCRTResidues line 175
  17. theorem OAI.Erdos970.ErdosInverseCRT.integerCRTResidues_card line 179
  18. theorem OAI.Erdos970.ErdosInverseCRT.integerCRTResidues_subset line 189
  19. theorem OAI.Erdos970.ErdosInverseCRT.emod_mem_integerCRTResidues line 198
  20. theorem OAI.Erdos970.ErdosInverseCRT.product_card_le_moduli line 212
  21. def OAI.Erdos970.Erdos66Dependency.ResidueLifts.liftsOn line 228
  22. theorem OAI.Erdos970.Erdos66Dependency.ResidueLifts.lifts_eq_union line 231
  23. theorem OAI.Erdos970.Erdos66Dependency.ResidueLifts.classes_disjoint line 244
  24. theorem OAI.Erdos970.Erdos66Dependency.ResidueLifts.count_eq_sum line 257
  25. theorem OAI.Erdos970.Erdos66Dependency.ResidueLifts.count_error line 261
  26. lemma OAI.Erdos970.Erdos66Dependency.ResidueLifts.card_Ico_real line 275
  27. theorem OAI.Erdos970.Erdos66Dependency.ResidueLifts.count_error_length line 281
  28. theorem OAI.Erdos970.Erdos66Dependency.ResidueLifts.count_error_Icc line 286
  29. theorem OAI.Erdos970.Erdos66Dependency.ResidueLifts.count_error_Ioc line 292
  30. theorem OAI.Erdos970.Erdos66Dependency.ResidueLifts.count_error_Ioo line 298
  31. def OAI.Erdos970.ErdosInverseCRT.crtSlopes line 313
  32. theorem OAI.Erdos970.ErdosInverseCRT.crtSlopes_eq_lifts line 317
  33. theorem OAI.Erdos970.ErdosInverseCRT.crt_interval_count_upper line 324
  34. theorem OAI.Erdos970.ErdosInverseCRT.crt_initial_count_upper line 337
  35. abbrev OAI.Erdos970.ErdosCoprimeResidueInterval.binaryModuli line 352
  36. theorem OAI.Erdos970.ErdosCoprimeResidueInterval.binary_coprime line 356
  37. def OAI.Erdos970.ErdosCoprimeResidueInterval.binaryClasses line 365
  38. theorem OAI.Erdos970.ErdosCoprimeResidueInterval.binary_modulus_product line 370
  39. def OAI.Erdos970.ErdosCoprimeResidueInterval.divisibleResidues line 373
  40. theorem OAI.Erdos970.ErdosCoprimeResidueInterval.divisibleResidues_card line 376
  41. theorem OAI.Erdos970.ErdosCoprimeResidueInterval.divisibleResidues_range line 383
  42. theorem OAI.Erdos970.ErdosCoprimeResidueInterval.mem_divisibleResidues line 390
  43. theorem OAI.Erdos970.ErdosCoprimeResidueInterval.divisible_residue_count line 400
  44. def OAI.Erdos970.ErdosInverseCRT.affineEquiv line 421
  45. def OAI.Erdos970.ErdosInverseCRT.affineResidues line 433
  46. theorem OAI.Erdos970.ErdosInverseCRT.mem_affineResidues line 436
  47. theorem OAI.Erdos970.ErdosInverseCRT.affineResidues_card line 448
  48. theorem OAI.Erdos970.ErdosInverseCRT.source_edge_class_affine line 451
  49. def OAI.Erdos970.ErdosCoprimeResidueInterval.coprimeResidues line 470
  50. theorem OAI.Erdos970.ErdosCoprimeResidueInterval.coprime_residue_count line 473
  51. theorem OAI.Erdos970.ErdosCoprimeResidueInterval.coprime_residue_count_length line 518
  52. def OAI.Erdos970.ErdosCoprimeResidueInterval.realCoprimeResidues line 533
  53. theorem OAI.Erdos970.ErdosCoprimeResidueInterval.mem_realCoprimeResidues line 536
  54. theorem OAI.Erdos970.ErdosCoprimeResidueInterval.ceiling_interval_error line 542
  55. theorem OAI.Erdos970.ErdosCoprimeResidueInterval.coprime_density_bounds line 547
  56. theorem OAI.Erdos970.ErdosCoprimeResidueInterval.real_coprime_residue_count line 557