OAI/NumberTheory/DirichletL/Hecke/Strip.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.HeckeStrip.gammaConstant line 12
  2. theorem OAI.SevenEighths.HeckeStrip.gammaConstant_pos line 14
  3. theorem OAI.SevenEighths.HeckeStrip.gamma_ratio_left_bound line 17
  4. theorem OAI.SevenEighths.HeckeStrip.gamma_ratio_left_bound_of_re line 48
  5. def OAI.SevenEighths.HeckeStrip.completionScale line 55
  6. theorem OAI.SevenEighths.HeckeStrip.completionScale_pos line 57
  7. theorem OAI.SevenEighths.HeckeStrip.completionScale_left_power line 61
  8. def OAI.SevenEighths.HeckeStrip.leftConstant line 73
  9. theorem OAI.SevenEighths.HeckeStrip.leftConstant_pos line 76
  10. theorem OAI.SevenEighths.HeckeStrip.left_boundary_of_functional_equation line 79
  11. def OAI.SevenEighths.HeckeStrip.strip line 105
  12. def OAI.SevenEighths.HeckeStrip.closedStrip line 106
  13. theorem OAI.SevenEighths.HeckeStrip.vertical_strip_of_exp_bound line 108
  14. theorem OAI.SevenEighths.HeckeStrip.closure_strip_subset line 129
  15. theorem OAI.SevenEighths.HeckeStrip.shift_norm_lower line 133
  16. theorem OAI.SevenEighths.HeckeStrip.shift_ne_zero line 138
  17. theorem OAI.SevenEighths.HeckeStrip.height_le_shift_norm line 144
  18. theorem OAI.SevenEighths.HeckeStrip.shift_norm_le_height line 151
  19. def OAI.SevenEighths.HeckeStrip.normalized line 158
  20. theorem OAI.SevenEighths.HeckeStrip.norm_normalized line 161
  21. theorem OAI.SevenEighths.HeckeStrip.normalized_diffContOnCl line 166
  22. theorem OAI.SevenEighths.HeckeStrip.normalized_exp_bound line 178
  23. theorem OAI.SevenEighths.HeckeStrip.normalized_boundary_bound line 197
  24. theorem OAI.SevenEighths.HeckeStrip.uniform_strip_bound_of_edges line 212
  25. theorem OAI.SevenEighths.HeckeStrip.uniform_strip_bound line 241
  26. theorem OAI.SevenEighths.HeckeStrip.uniform_strip_bound_of_functional_equation line 260
  27. theorem OAI.SevenEighths.HeckeStrip.uncompleted_exp_bound line 284
  28. theorem OAI.SevenEighths.HeckeStrip.mellin_uncompleted_exp_bound line 307