OAI/NumberTheory/Jacobsthal/Sieve/ExponentialMesh.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.ExponentialMesh.mesh line 16
  2. theorem OAI.Erdos970.NumberTheoryLean.ExponentialMesh.mesh_pos line 18
  3. theorem OAI.Erdos970.NumberTheoryLean.ExponentialMesh.mesh_upper line 22
  4. theorem OAI.Erdos970.NumberTheoryLean.ExponentialMesh.mesh_reciprocal line 31
  5. theorem OAI.Erdos970.NumberTheoryLean.ExponentialMesh.reciprocal_upper line 35
  6. theorem OAI.Erdos970.NumberTheoryLean.ExponentialMesh.mesh_le_one line 42
  7. theorem OAI.Erdos970.NumberTheoryLean.ExponentialMesh.half_sqrt_lower line 47
  8. theorem OAI.Erdos970.NumberTheoryLean.ExponentialMesh.prime_error_dominated line 52
  9. theorem OAI.Erdos970.NumberTheoryLean.ExponentialMesh.prime_error_over_mesh line 61
  10. theorem OAI.Erdos970.NumberTheoryLean.ExponentialMesh.log_pow_sqrt line 78
  11. theorem OAI.Erdos970.NumberTheoryLean.ExponentialMesh.log_power_exp_tendsto line 82
  12. theorem OAI.Erdos970.NumberTheoryLean.ExponentialMesh.log_power_exp_absorption line 91
  13. theorem OAI.Erdos970.NumberTheoryLean.ExponentialMesh.exp_increment line 105