OAI/NumberTheory/DirichletL/Hecke/LogarithmicInput.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.HeckeLogarithmicInput.regular line 11
  2. theorem OAI.SevenEighths.HeckeLogarithmicInput.regular_eq_nonprincipal line 14
  3. theorem OAI.SevenEighths.HeckeLogarithmicInput.regular_differentiableAt line 17
  4. theorem OAI.SevenEighths.HeckeLogarithmicInput.regular_ne_zero line 32
  5. theorem OAI.SevenEighths.HeckeLogarithmicInput.regular_inverse_differentiableAt line 52
  6. theorem OAI.SevenEighths.HeckeLogarithmicInput.principal_regular_factor_bound line 58
  7. theorem OAI.SevenEighths.HeckeLogarithmicInput.regular_norm_le line 66
  8. theorem OAI.SevenEighths.HeckeLogarithmicInput.regular_inverse_norm_le line 83
  9. def OAI.SevenEighths.HeckeLogarithmicInput.uniformConstant line 109
  10. theorem OAI.SevenEighths.HeckeLogarithmicInput.uniformConstant_nonneg line 112
  11. theorem OAI.SevenEighths.HeckeLogarithmicInput.modulus_norm_ge_one line 118
  12. theorem OAI.SevenEighths.HeckeLogarithmicInput.regular_strip_bound line 122
  13. theorem OAI.SevenEighths.HeckeLogarithmicInput.regular_right_growth line 137
  14. theorem OAI.SevenEighths.HeckeLogarithmicInput.regular_ne_zero_on_disk line 155
  15. theorem OAI.SevenEighths.HeckeLogarithmicInput.reciprocal_norm_le_regular_inverse line 167
  16. theorem OAI.SevenEighths.HeckeLogarithmicInput.regular_disk_growth line 195