OAI/NumberTheory/SiegelZeros/Differentials/ZetaLogDerivative.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SiegelZeros.Awei.W53.zetaPoleRemoved line 20
2. theorem OAI.SiegelZeros.Awei.W53.zetaPoleRemoved_one line 23
3. theorem OAI.SiegelZeros.Awei.W53.analyticAt_zetaPoleRemoved line 26
4. theorem OAI.SiegelZeros.Awei.W53.zetaPoleRemoved_eq line 33
5. theorem OAI.SiegelZeros.Awei.W53.deriv_zetaPoleRemoved line 44
6. theorem OAI.SiegelZeros.Awei.W53.zeta_logDerivative_identity line 53
7. theorem OAI.SiegelZeros.Awei.W53.zetaPoleRemoved_ne_zero_real line 62
8. theorem OAI.SiegelZeros.Awei.W53.zeta_logDerivative_uniform_bound line 72
9. theorem OAI.SiegelZeros.Awei.W53.zeta_logDerivative_re_upper line 90