OAI/NumberTheory/Jacobsthal/Sieve/IntervalBoundingSieve.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.IntervalBoundingSieve.reciprocalDensity line 18
  2. theorem OAI.Erdos970.NumberTheoryLean.IntervalBoundingSieve.reciprocalDensity_apply line 22
  3. theorem OAI.Erdos970.NumberTheoryLean.IntervalBoundingSieve.reciprocalDensity_multiplicative line 25
  4. def OAI.Erdos970.NumberTheoryLean.IntervalBoundingSieve.intervalSieve line 30
  5. theorem OAI.Erdos970.NumberTheoryLean.IntervalBoundingSieve.interval_multSum line 46
  6. theorem OAI.Erdos970.NumberTheoryLean.IntervalBoundingSieve.interval_siftedSum line 58
  7. theorem OAI.Erdos970.NumberTheoryLean.IntervalBoundingSieve.interval_rem_abs_le_one line 70
  8. theorem OAI.Erdos970.NumberTheoryLean.IntervalBoundingSieve.coprime_count_le_upperMoebius line 88
  9. theorem OAI.Erdos970.NumberTheoryLean.IntervalBoundingSieve.exists_residue_translation line 111
  10. def OAI.Erdos970.NumberTheoryLean.IntervalBoundingSieve.residueAvoidingOffsets line 139
  11. theorem OAI.Erdos970.NumberTheoryLean.IntervalBoundingSieve.exists_residue_count_translation line 144
  12. theorem OAI.Erdos970.NumberTheoryLean.IntervalBoundingSieve.residue_count_le_upperMoebius line 158
  13. theorem OAI.Erdos970.NumberTheoryLean.IntervalBoundingSieve.squarefree_primeSet_product line 168
  14. def OAI.Erdos970.NumberTheoryLean.IntervalBoundingSieve.cutoffProduct line 185
  15. theorem OAI.Erdos970.NumberTheoryLean.IntervalBoundingSieve.cutoffProduct_squarefree line 187
  16. theorem OAI.Erdos970.NumberTheoryLean.IntervalBoundingSieve.cutoffProduct_primeFactors line 192
  17. theorem OAI.Erdos970.NumberTheoryLean.IntervalBoundingSieve.cutoffSurvivors_card_le_upperMoebius line 198