OAI/NumberTheory/Jacobsthal/Sieve/AlignedPrimeCongruence.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.SievePartition.survivors line 24
  2. def OAI.Erdos970.NumberTheoryLean.SievePartition.childCell line 29
  3. theorem OAI.Erdos970.NumberTheoryLean.SievePartition.mem_survivors line 35
  4. theorem OAI.Erdos970.NumberTheoryLean.SievePartition.mem_childCell line 42
  5. theorem OAI.Erdos970.NumberTheoryLean.SievePartition.exists_childCell line 51
  6. theorem OAI.Erdos970.NumberTheoryLean.SievePartition.childCell_disjoint line 73
  7. theorem OAI.Erdos970.NumberTheoryLean.SievePartition.biUnion_childCell line 86
  8. theorem OAI.Erdos970.NumberTheoryLean.SievePartition.sum_card_childCell line 101
  9. theorem OAI.Erdos970.NumberTheoryLean.SievePartition.card_survivors_add_sum line 109
  10. theorem OAI.Erdos970.NumberTheoryLean.SievePartition.card_survivors_eq_sub_sum line 115
  11. def OAI.Erdos970.NumberTheoryLean.SievePartition.residueBad line 124
  12. instance OAI.Erdos970.NumberTheoryLean.SievePartition.decidableResidueBad line 126
  13. def OAI.Erdos970.NumberTheoryLean.SievePartition.residueCandidates line 129
  14. theorem OAI.Erdos970.NumberTheoryLean.SievePartition.mem_residueCandidates line 135
  15. theorem OAI.Erdos970.NumberTheoryLean.SievePartition.residueCandidates_insert line 144
  16. theorem OAI.Erdos970.NumberTheoryLean.SievePartition.residue_childCell_eq line 154
  17. theorem OAI.Erdos970.NumberTheoryLean.SievePartition.residue_tree_identity line 169
  18. structure OAI.Erdos970.NumberTheoryLean.SieveTree.Data line 191
  19. def OAI.Erdos970.NumberTheoryLean.SieveTree.bounds line 201
  20. theorem OAI.Erdos970.NumberTheoryLean.SieveTree.survivors_le_mass line 208
  21. theorem OAI.Erdos970.NumberTheoryLean.SieveTree.bounds_correct line 215
  22. theorem OAI.Erdos970.NumberTheoryLean.SieveTree.stopped_tree_lower_bound line 241
  23. theorem OAI.Erdos970.NumberTheoryLean.SieveTree.exact_lower_stop line 245
  24. theorem OAI.Erdos970.NumberTheoryLean.SieveTree.leaf_mass_eq line 250
  25. abbrev OAI.Erdos970.NumberTheoryLean.ResidueSieveTree.Vertex line 265
  26. def OAI.Erdos970.NumberTheoryLean.ResidueSieveTree.child line 267
  27. def OAI.Erdos970.NumberTheoryLean.ResidueSieveTree.children line 270
  28. def OAI.Erdos970.NumberTheoryLean.ResidueSieveTree.retained line 272
  29. theorem OAI.Erdos970.NumberTheoryLean.ResidueSieveTree.retained_subset line 276
  30. theorem OAI.Erdos970.NumberTheoryLean.ResidueSieveTree.child_injOn line 281
  31. theorem OAI.Erdos970.NumberTheoryLean.ResidueSieveTree.child_card_lt line 294
  32. def OAI.Erdos970.NumberTheoryLean.ResidueSieveTree.mass line 299
  33. def OAI.Erdos970.NumberTheoryLean.ResidueSieveTree.survivorCount line 302
  34. theorem OAI.Erdos970.NumberTheoryLean.ResidueSieveTree.survivorCount_nonneg line 306
  35. theorem OAI.Erdos970.NumberTheoryLean.ResidueSieveTree.partition line 309
  36. def OAI.Erdos970.NumberTheoryLean.ResidueSieveTree.data line 316
  37. theorem OAI.Erdos970.NumberTheoryLean.ResidueSieveTree.bounds_correct line 327
  38. theorem OAI.Erdos970.NumberTheoryLean.ResidueSieveTree.stopped_tree_lower_bound line 335
  39. theorem OAI.Erdos970.NumberTheoryLean.ResidueSieveTree.bounds_succ_eq_of_card_le line 341
  40. theorem OAI.Erdos970.NumberTheoryLean.ResidueSieveTree.bounds_stabilize line 381
  41. def OAI.Erdos970.ErdosInverseCounts.modulusCandidates line 401
  42. def OAI.Erdos970.ErdosInverseCounts.modulusCount line 404
  43. theorem OAI.Erdos970.ErdosInverseCounts.mem_modulusCandidates line 407
  44. theorem OAI.Erdos970.ErdosInverseCounts.modulusCount_eq_mass line 412
  45. theorem OAI.Erdos970.ErdosInverseCounts.modulusCount_nonneg line 415
  46. theorem OAI.Erdos970.ErdosInverseCounts.modulusCandidates_prime_mul line 418
  47. theorem OAI.Erdos970.ErdosInverseCounts.primeFactors_product line 426
  48. theorem OAI.Erdos970.ErdosInverseCounts.modulusCount_product_eq_mass line 440
  49. theorem OAI.Erdos970.ErdosAlignedProgression.aligned_den_coprime_prime line 454
  50. theorem OAI.Erdos970.ErdosAlignedProgression.aligned_den_coprime line 458
  51. theorem OAI.Erdos970.ErdosAlignedProgression.aligned_prime_hit_iff line 464
  52. theorem OAI.Erdos970.ErdosAlignedProgression.squarefree_int_modEq_iff line 484
  53. theorem OAI.Erdos970.ErdosAlignedProgression.required_hits_iff_parameter line 492