OAI/NumberTheory/SiegelZeros/EntireFunctions/GammaBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SiegelZeros.SiegelZerosAwei.W52.gammaLogDerivative line 13
2. theorem OAI.SiegelZeros.SiegelZerosAwei.W52.analyticAt_Gamma_of_re_pos line 16
3. theorem OAI.SiegelZeros.SiegelZerosAwei.W52.continuousAt_gammaLogDerivative line 30
4. theorem OAI.SiegelZeros.SiegelZerosAwei.W52.exists_gammaLogDerivative_bound line 35
5. theorem OAI.SiegelZeros.SiegelZerosAwei.W52.exists_uniform_parity_gamma_bound line 51