OAI/NumberTheory/DirichletL/PrincipalMellinResidues.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.PrincipalMellinResidues.inverse_vertical_continuous line 16
  2. lemma OAI.SevenEighths.PrincipalMellinResidues.inverse_vertical_truncated line 24
  3. lemma OAI.SevenEighths.PrincipalMellinResidues.inverse_vertical_limit_pos line 51
  4. lemma OAI.SevenEighths.PrincipalMellinResidues.inverse_vertical_limit_neg line 58
  5. lemma OAI.SevenEighths.PrincipalMellinResidues.inverse_horizontal_limit line 65
  6. lemma OAI.SevenEighths.PrincipalMellinResidues.dslope_eq_sub_pole line 81
  7. lemma OAI.SevenEighths.PrincipalMellinResidues.dslope_vertical_truncated line 88
  8. lemma OAI.SevenEighths.PrincipalMellinResidues.rectangle_limits line 106
  9. lemma OAI.SevenEighths.PrincipalMellinResidues.horizontal_quotient_continuousOn line 129
  10. lemma OAI.SevenEighths.PrincipalMellinResidues.dslope_horizontal_limit line 142
  11. theorem OAI.SevenEighths.PrincipalMellinResidues.verticalIntegral_simple_pole line 173
  12. structure OAI.SevenEighths.PrincipalMellinResidues.BoundaryControl line 221
  13. theorem OAI.SevenEighths.PrincipalMellinResidues.verticalIntegral_hecke line 229
  14. theorem OAI.SevenEighths.PrincipalMellinResidues.verticalIntegral_hecke_six line 249
  15. theorem OAI.SevenEighths.PrincipalMellinResidues.source_w_shift line 282
  16. theorem OAI.SevenEighths.PrincipalMellinResidues.source_residue_z_shift line 292
  17. lemma OAI.SevenEighths.PrincipalMellinResidues.verticalIntegral_add line 300
  18. lemma OAI.SevenEighths.PrincipalMellinResidues.verticalIntegral_mul_const line 307
  19. theorem OAI.SevenEighths.PrincipalMellinResidues.source_ordered_double_shift line 313
  20. abbrev OAI.SevenEighths.PrincipalMellinResidues.fixedPrincipal line 349
  21. def OAI.SevenEighths.PrincipalMellinResidues.fixedPrincipalResidue line 352
  22. theorem OAI.SevenEighths.PrincipalMellinResidues.fixedPrincipalResidue_ne_zero line 355
  23. def OAI.SevenEighths.PrincipalMellinResidues.sourceMultiplier line 360
  24. theorem OAI.SevenEighths.PrincipalMellinResidues.sourceMultiplier_integrand line 367
  25. def OAI.SevenEighths.PrincipalMellinResidues.sourceResidueConstant line 379
  26. theorem OAI.SevenEighths.PrincipalMellinResidues.source_double_residue line 383
  27. theorem OAI.SevenEighths.PrincipalMellinResidues.source_axes_separated line 396