OAI/NumberTheory/PrimeGaps/AdditiveSieve.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LargePrimeGaps.symmetric_kernel_quadratic_le line 29
2. theorem OAI.LargePrimeGaps.norm_sum_smul_sq_le_gram line 56
3. theorem OAI.LargePrimeGaps.gram_large_sieve line 82
4. def OAI.LargePrimeGaps.bvExp line 118
5. theorem OAI.LargePrimeGaps.bvExp_zero line 120
6. theorem OAI.LargePrimeGaps.norm_bvExp line 122
7. theorem OAI.LargePrimeGaps.bvExp_add line 124
8. theorem OAI.LargePrimeGaps.conj_bvExp line 131
9. theorem OAI.LargePrimeGaps.bvExp_nat_mul line 139
10. theorem OAI.LargePrimeGaps.bvExp_sub_one_lower line 146
11. theorem OAI.LargePrimeGaps.exponential_sum_bound line 161
12. theorem OAI.LargePrimeGaps.reciprocal_sum_le_harmonic line 179
13. theorem OAI.LargePrimeGaps.reciprocal_sum_le_scaled_harmonic line 213
14. theorem OAI.LargePrimeGaps.bvExp_int line 236
15. theorem OAI.LargePrimeGaps.bvExp_sub_int line 243
16. def OAI.LargePrimeGaps.bvCentered line 248
17. theorem OAI.LargePrimeGaps.abs_bvCentered_le line 250
18. theorem OAI.LargePrimeGaps.bvExp_centered line 256
19. theorem OAI.LargePrimeGaps.exponential_sum_centered line 258
20. theorem OAI.LargePrimeGaps.centered_difference_separated line 263
21. theorem OAI.LargePrimeGaps.exponential_kernel_row_bound line 273
22. def OAI.LargePrimeGaps.bvExponentialVector line 334
23. theorem OAI.LargePrimeGaps.inner_bvExponentialVector line 337
24. theorem OAI.LargePrimeGaps.inner_bvExponentialVector_coefficients line 349
25. theorem OAI.LargePrimeGaps.additive_large_sieve line 359
26. theorem OAI.LargePrimeGaps.rat_abs_lower line 392
27. theorem OAI.LargePrimeGaps.rational_frequency_separation line 399
28. theorem OAI.LargePrimeGaps.rational_additive_large_sieve line 425