OAI/NumberTheory/Jacobsthal/Sieve/PrimeExponentialTail.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.ExponentialMeshTail.quadratic_exp_majorant line 15
2. def OAI.Erdos970.NumberTheoryLean.ExponentialMeshTail.envelope line 28
3. theorem OAI.Erdos970.NumberTheoryLean.ExponentialMeshTail.reward_le_envelope line 31
4. theorem OAI.Erdos970.NumberTheoryLean.ExponentialMeshTail.exponential_mesh_sum line 40
5. theorem OAI.Erdos970.NumberTheoryLean.ExponentialMeshTail.envelope_mesh_sum line 70
6. def OAI.Erdos970.NumberTheoryLean.PrimeExponentialTail.tailReward line 108
7. theorem OAI.Erdos970.NumberTheoryLean.PrimeExponentialTail.grid_above line 113
8. theorem OAI.Erdos970.NumberTheoryLean.PrimeExponentialTail.actual_tail_bin_envelope line 122
9. theorem OAI.Erdos970.NumberTheoryLean.PrimeExponentialTail.actual_tail_integral_bins line 155
10. theorem OAI.Erdos970.NumberTheoryLean.PrimeExponentialTail.actual_tail_from_inverse_bins line 173