OAI/NumberTheory/SiegelZeros/EntireFunctions/IndexedProduct.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SiegelZeros.SiegelZerosAwei.W03.genusOneFactor line 21
2. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.differentiable_genusOneFactor line 24
3. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.genusOneFactor_ne_zero line 29
4. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.logDeriv_genusOneFactor line 36
5. def OAI.SiegelZeros.SiegelZerosAwei.W03.zeroFactor line 56
6. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.differentiable_zeroFactor line 59
7. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.zeroFactor_ne_zero line 63
8. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.logDeriv_zeroFactor line 67
9. def OAI.SiegelZeros.SiegelZerosAwei.W03.NonzeroZero line 73
10. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.logDeriv_canonicalProduct line 75
11. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.regularized_reciprocal_eq line 113
12. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.norm_regularized_reciprocal_le line 118
13. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.summable_regularized_actual_zeros line 134
14. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.norm_primaryFactor_sub_one_le line 160
15. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.norm_genusOneFactor_sub_one_le line 174
16. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.multipliableLocallyUniformlyOn_genusOne line 188
17. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.summable_norm_genusOneFactor_sub_one line 206
18. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.genusOneProduct_ne_zero line 215
19. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.reciprocal_re_bounds line 234
20. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.summable_reciprocal_re line 240
21. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.summable_real_zero_contributions line 248
22. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.real_regularized_tsum line 256
23. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.logDeriv_indexedGenusOneProduct line 272