OAI/NumberTheory/Jacobsthal/Sieve/ResidueCountDifference.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.NumberTheoryLean.ProgressionSieve.exists_affine_residue line 15
  2. theorem OAI.Erdos970.NumberTheoryLean.ProgressionSieve.exists_progression_residues line 35
  3. theorem OAI.Erdos970.NumberTheoryLean.ProgressionSieve.divisibilityResidue_lt line 51
  4. theorem OAI.Erdos970.NumberTheoryLean.ProgressionSieve.offset_eq_residue_add_mul_div line 59
  5. def OAI.Erdos970.NumberTheoryLean.ProgressionSieve.progressionLength line 70
  6. theorem OAI.Erdos970.NumberTheoryLean.ProgressionSieve.exists_deletion_pullback line 72
  7. def OAI.Erdos970.NumberTheoryLean.ProgressionSieve.deletionBudget line 103
  8. theorem OAI.Erdos970.NumberTheoryLean.ProgressionSieve.deletionBudget_nonneg line 106
  9. theorem OAI.Erdos970.NumberTheoryLean.ProgressionSieve.largePrime_deletion_le_log line 114
  10. theorem OAI.Erdos970.NumberTheoryLean.ProgressionSieve.sum_largePrime_deletions_le_log line 125
  11. theorem OAI.Erdos970.NumberTheoryLean.ProgressionSieve.isJacobsthalBound_of_cutoff_lower line 144
  12. theorem OAI.Erdos970.NumberTheoryLean.SmallSieveRelative.normalized_remainder_le line 164
  13. theorem OAI.Erdos970.NumberTheoryLean.SmallSieveRelative.relative_bound_rpow line 191
  14. theorem OAI.Erdos970.NumberTheoryLean.SmallSieveRelative.rpow_log_ratio line 217
  15. theorem OAI.Erdos970.NumberTheoryLean.SmallSieveRelative.small_relative line 224
  16. def OAI.Erdos970.NumberTheoryLean.ProgressionSmallSieve.progressionHit line 240
  17. def OAI.Erdos970.NumberTheoryLean.ProgressionSmallSieve.progressionSurvivors line 243
  18. theorem OAI.Erdos970.NumberTheoryLean.ProgressionSmallSieve.exists_integer_affine_residue line 247
  19. theorem OAI.Erdos970.NumberTheoryLean.ProgressionSmallSieve.exists_coordinate_residues line 269
  20. theorem OAI.Erdos970.NumberTheoryLean.ProgressionSmallSieve.exists_progressionSurvivors_eq line 284
  21. theorem OAI.Erdos970.NumberTheoryLean.ProgressionSmallSieve.progression_small_relative line 300
  22. def OAI.Erdos970.ErdosModulusRelative.modulusOffsets line 322
  23. theorem OAI.Erdos970.ErdosModulusRelative.modulus_candidates_eq_offsets line 327
  24. theorem OAI.Erdos970.ErdosModulusRelative.modulus_count_eq_offsets line 347
  25. theorem OAI.Erdos970.ErdosModulusRelative.offsets_eq_progression line 355
  26. theorem OAI.Erdos970.ErdosModulusRelative.large_modulus_coprime_small line 371
  27. theorem OAI.Erdos970.NumberTheoryLean.SmallSieveUpper.cutoffSurvivors_antitone line 386
  28. theorem OAI.Erdos970.NumberTheoryLean.SmallSieveUpper.count_le_four_of_relative line 392
  29. theorem OAI.Erdos970.NumberTheoryLean.SmallSieveUpper.threshold_ge_two line 409
  30. theorem OAI.Erdos970.NumberTheoryLean.SmallSieveUpper.small_upper_explicit line 414
  31. theorem OAI.Erdos970.NumberTheoryLean.SmallSieveUpper.small_upper line 452
  32. theorem OAI.Erdos970.NumberTheoryLean.SmallSieveUpper.progression_small_upper line 468
  33. def OAI.Erdos970.ErdosPrimeInputs.SubsetPrimeSieve.euler line 495
  34. theorem OAI.Erdos970.ErdosPrimeInputs.SubsetPrimeSieve.finite_subset_sieve_bound line 497
  35. theorem OAI.Erdos970.ErdosPrimeInputs.SubsetPrimeSieve.euler_pos line 526
  36. theorem OAI.Erdos970.ErdosModulusRelative.modulus_small_relative line 539
  37. theorem OAI.Erdos970.ErdosModulusRelative.uniform_modulus_small_relative line 557
  38. def OAI.Erdos970.ErdosInverseTail.sieveTail line 588
  39. theorem OAI.Erdos970.ErdosInverseTail.progressionHit_shift line 592
  40. theorem OAI.Erdos970.ErdosInverseTail.sieveTail_eq_image line 600
  41. theorem OAI.Erdos970.ErdosInverseTail.sieveTail_card line 615
  42. theorem OAI.Erdos970.ErdosInverseTail.survivor_card_split line 621
  43. def OAI.Erdos970.ErdosInverseTail.residueOffset line 653
  44. theorem OAI.Erdos970.ErdosInverseTail.residueOffset_lt line 655
  45. theorem OAI.Erdos970.ErdosInverseTail.residue_coordinate_exists line 657
  46. theorem OAI.Erdos970.ErdosInverseTail.residue_coordinate_hit line 668
  47. theorem OAI.Erdos970.ErdosInverseTail.progressionHit_stride line 674
  48. theorem OAI.Erdos970.ErdosInverseTail.residue_tail_eq_image line 682
  49. theorem OAI.Erdos970.ErdosInverseTail.residue_tail_card line 707
  50. theorem OAI.Erdos970.ErdosInverseTail.residue_survivor_card_split line 723
  51. theorem OAI.Erdos970.ErdosInverseTail.residue_count_difference line 750