OAI/NumberTheory/Jacobsthal/Sieve/TagUnitSieveLower.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosStoppedTagSieve.primeFactor line 17
  2. def OAI.Erdos970.ErdosStoppedTagSieve.eulerWeight line 18
  3. lemma OAI.Erdos970.ErdosStoppedTagSieve.shifted_nonneg line 20
  4. lemma OAI.Erdos970.ErdosStoppedTagSieve.shifted_le_one line 26
  5. lemma OAI.Erdos970.ErdosStoppedTagSieve.shifted_product line 30
  6. theorem OAI.Erdos970.ErdosStoppedTagSieve.eulerWeight_lower line 42
  7. lemma OAI.Erdos970.ErdosStoppedTagSieve.primeFactor_nonneg line 82
  8. lemma OAI.Erdos970.ErdosStoppedTagSieve.primeFactor_le_one line 89
  9. lemma OAI.Erdos970.ErdosStoppedTagSieve.eulerWeight_nonneg line 95
  10. lemma OAI.Erdos970.ErdosStoppedTagSieve.eulerWeight_le_one line 98
  11. lemma OAI.Erdos970.ErdosStoppedTagSieve.eulerWeight_eq_zero_of_two line 102
  12. lemma OAI.Erdos970.ErdosStoppedTagSieve.odd_of_eulerWeight_ne_zero line 106
  13. lemma OAI.Erdos970.ErdosStoppedTagSieve.reciprocal_totient_density_le line 115
  14. def OAI.Erdos970.ErdosStoppedTagSieve.basePrimes line 129
  15. def OAI.Erdos970.ErdosStoppedTagSieve.survivorPrimes line 131
  16. lemma OAI.Erdos970.ErdosStoppedTagSieve.actual_intersection_mass line 135
  17. lemma OAI.Erdos970.ErdosStoppedTagSieve.actual_survivor_mass line 150
  18. theorem OAI.Erdos970.ErdosStoppedTagSieve.finite_tag_sieve_error line 160
  19. theorem OAI.Erdos970.ErdosStoppedTagSieve.unit_lift_sieve_lower_eventually line 232