OAI/NumberTheory/Jacobsthal/Sieve/SieveScale.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosPrimeInputs.AffinePrimeSieve.value line 16
  2. def OAI.Erdos970.ErdosPrimeInputs.AffinePrimeSieve.survivors line 17
  3. def OAI.Erdos970.ErdosPrimeInputs.AffinePrimeSieve.primeIndices line 19
  4. def OAI.Erdos970.ErdosPrimeInputs.AffinePrimeSieve.smallPrimeIndices line 21
  5. theorem OAI.Erdos970.ErdosPrimeInputs.AffinePrimeSieve.exists_coordinate_residues line 24
  6. theorem OAI.Erdos970.ErdosPrimeInputs.AffinePrimeSieve.affine_sieve_error line 45
  7. lemma OAI.Erdos970.ErdosPrimeInputs.AffinePrimeSieve.natAbs_cast_of_nonneg line 55
  8. theorem OAI.Erdos970.ErdosPrimeInputs.AffinePrimeSieve.prime_above_survives line 58
  9. theorem OAI.Erdos970.ErdosPrimeInputs.AffinePrimeSieve.value_injective line 73
  10. theorem OAI.Erdos970.ErdosPrimeInputs.AffinePrimeSieve.small_prime_count_le line 79
  11. theorem OAI.Erdos970.ErdosPrimeInputs.AffinePrimeSieve.prime_count_le_sifted_add line 104
  12. def OAI.Erdos970.ErdosPrimeInputs.SieveScale.level line 130
  13. def OAI.Erdos970.ErdosPrimeInputs.SieveScale.exponent line 131
  14. def OAI.Erdos970.ErdosPrimeInputs.SieveScale.cutoff line 132
  15. lemma OAI.Erdos970.ErdosPrimeInputs.SieveScale.exponent_pos line 134
  16. lemma OAI.Erdos970.ErdosPrimeInputs.SieveScale.exponent_le_half line 135
  17. lemma OAI.Erdos970.ErdosPrimeInputs.SieveScale.cutoff_tendsto line 137
  18. lemma OAI.Erdos970.ErdosPrimeInputs.SieveScale.cutoff_eventually_ge line 139
  19. lemma OAI.Erdos970.ErdosPrimeInputs.SieveScale.cutoff_power line 145
  20. lemma OAI.Erdos970.ErdosPrimeInputs.SieveScale.log_cutoff line 150
  21. lemma OAI.Erdos970.ErdosPrimeInputs.SieveScale.cutoff_le_sqrt line 153
  22. lemma OAI.Erdos970.ErdosPrimeInputs.SieveScale.sqrt_le_log_scale line 157