OAI/NumberTheory/Jacobsthal/Primes/PrimeCountAbel.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.ErdosPrimeInputs.PrimeCountingPrimitive.scale line 19
2. def OAI.Erdos970.ErdosPrimeInputs.PrimeCountingPrimitive.kernel line 20
3. def OAI.Erdos970.ErdosPrimeInputs.PrimeCountingPrimitive.slope line 21
4. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeCountingPrimitive.scale_nonneg line 24
5. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeCountingPrimitive.hasDerivAt_scale line 27
6. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeCountingPrimitive.kernel_le_slope line 37
7. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeCountingPrimitive.continuousOn_kernel line 53
8. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeCountingPrimitive.continuousOn_slope line 62
9. theorem OAI.Erdos970.ErdosPrimeInputs.PrimeCountingPrimitive.integral_kernel_le line 73
10. theorem OAI.Erdos970.ErdosPrimeInputs.PrimeCountingPrimitive.eventually_one_le_scale line 91
11. def OAI.Erdos970.ErdosPrimeInputs.PrimeCountAbel.logarithmicIntegral line 117
12. def OAI.Erdos970.ErdosPrimeInputs.PrimeCountAbel.primeError line 118
13. def OAI.Erdos970.ErdosPrimeInputs.PrimeCountAbel.endpoint line 119
14. def OAI.Erdos970.ErdosPrimeInputs.PrimeCountAbel.thetaKernel line 120
15. def OAI.Erdos970.ErdosPrimeInputs.PrimeCountAbel.mainKernel line 121
16. def OAI.Erdos970.ErdosPrimeInputs.PrimeCountAbel.errorKernel line 122
17. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeCountAbel.mainKernel_continuous line 124
18. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeCountAbel.mainKernel_integrable line 133
19. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeCountAbel.thetaKernel_integrable line 137
20. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeCountAbel.errorKernel_integrable line 142
21. lemma OAI.Erdos970.ErdosPrimeInputs.PrimeCountAbel.errorKernel_eq line 146
22. theorem OAI.Erdos970.ErdosPrimeInputs.PrimeCountAbel.primeError_eq line 151
23. theorem OAI.Erdos970.ErdosPrimeInputs.PrimeCountAbel.primeError_increment line 166