OAI/NumberTheory/Jacobsthal/Sieve/OriginalCofactorPoints.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosInverseRefinement.selectedRow line 17
  2. def OAI.Erdos970.ErdosInverseRefinement.rowReward line 21
  3. theorem OAI.Erdos970.ErdosInverseRefinement.selected_pairs_card_by_rows line 24
  4. theorem OAI.Erdos970.ErdosInverseRefinement.rowReward_bounds line 34
  5. theorem OAI.Erdos970.ErdosInverseRefinement.rowReward_sum line 43
  6. def OAI.Erdos970.ErdosInverseRefinement.richCofactors line 63
  7. theorem OAI.Erdos970.ErdosInverseRefinement.richCofactors_subset line 67
  8. theorem OAI.Erdos970.ErdosInverseRefinement.richCofactors_card_lower line 71
  9. theorem OAI.Erdos970.ErdosInverseRefinement.richCofactor_row_card line 79
  10. theorem OAI.Erdos970.ErdosInverseRefinement.richCofactors_source_size line 87
  11. def OAI.Erdos970.ErdosInverseRefinement.cofactorPoint line 108
  12. def OAI.Erdos970.ErdosInverseRefinement.cofactorPoints line 111
  13. theorem OAI.Erdos970.ErdosInverseRefinement.cofactorPoint_injective line 114
  14. theorem OAI.Erdos970.ErdosInverseRefinement.cofactorPoints_card line 120
  15. theorem OAI.Erdos970.ErdosInverseRefinement.cofactorPoints_x_injective line 124
  16. theorem OAI.Erdos970.ErdosInverseRefinement.cofactorPoints_square line 134
  17. theorem OAI.Erdos970.ErdosInverseRefinement.cofactorPoints_prime_hits line 146
  18. theorem OAI.Erdos970.ErdosInverseRefinement.rich_points_source_size line 158