OAI/NumberTheory/DirichletL/PrincipalMellinGrowth.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.PrincipalMellinGrowth.principalConstant line 13
  2. theorem OAI.SevenEighths.PrincipalMellinGrowth.principalConstant_pos line 17
  3. lemma OAI.SevenEighths.PrincipalMellinGrowth.poleRemoved_eq_mul_regular line 24
  4. theorem OAI.SevenEighths.PrincipalMellinGrowth.principal_poleRemoved_growth line 30
  5. def OAI.SevenEighths.PrincipalMellinGrowth.wAmplitude line 72
  6. def OAI.SevenEighths.PrincipalMellinGrowth.zAmplitude line 74
  7. theorem OAI.SevenEighths.PrincipalMellinGrowth.wAmplitude_pos line 76
  8. theorem OAI.SevenEighths.PrincipalMellinGrowth.zAmplitude_pos line 81
  9. theorem OAI.SevenEighths.PrincipalMellinGrowth.fixed_principal_w_growth line 85
  10. theorem OAI.SevenEighths.PrincipalMellinGrowth.fixed_principal_z_growth line 114
  11. theorem OAI.SevenEighths.PrincipalMellinGrowth.source_w_boundary line 144
  12. theorem OAI.SevenEighths.PrincipalMellinGrowth.source_z_boundary line 159