OAI/NumberTheory/DirichletL/Hecke/PrincipalStrip.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.HeckePrincipalStrip.normalized line 12
  2. theorem OAI.SevenEighths.HeckePrincipalStrip.normalized_diffContOnCl line 14
  3. theorem OAI.SevenEighths.HeckePrincipalStrip.norm_sub_one_le_shift line 21
  4. theorem OAI.SevenEighths.HeckePrincipalStrip.normalized_norm_le line 29
  5. theorem OAI.SevenEighths.HeckePrincipalStrip.norm_z_le_height line 37
  6. theorem OAI.SevenEighths.HeckePrincipalStrip.norm_sub_one_le_height line 43
  7. theorem OAI.SevenEighths.HeckePrincipalStrip.regularized_completion_bound line 50
  8. theorem OAI.SevenEighths.HeckePrincipalStrip.normalized_exp_growth line 79
  9. theorem OAI.SevenEighths.HeckePrincipalStrip.primitive_normalized_bound line 122
  10. theorem OAI.SevenEighths.HeckePrincipalStrip.poleRemoved_principalCharacter line 161
  11. theorem OAI.SevenEighths.HeckePrincipalStrip.uniform_normalized_strip_bound line 182
  12. def OAI.SevenEighths.HeckePrincipalStrip.sourceNormalized line 196
  13. theorem OAI.SevenEighths.HeckePrincipalStrip.sourceNormalized_norm_le line 199
  14. theorem OAI.SevenEighths.HeckePrincipalStrip.uniform_source_normalized_strip_bound line 219