OAI/NumberTheory/DirichletL/Hecke/Logarithmic.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.HeckeLogarithmic.complexity line 12
2. theorem OAI.SevenEighths.HeckeLogarithmic.complexity_ge_exp line 15
3. theorem OAI.SevenEighths.HeckeLogarithmic.regular_disk_differentiable line 18
4. theorem OAI.SevenEighths.HeckeLogarithmic.exists_uniform_polynomial_exponent line 26
5. theorem OAI.SevenEighths.HeckeLogarithmic.disk_control_of_euler_log line 48