OAI/NumberTheory/DirichletL/GammaZeroDetector.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.GammaZeroDetector.gamma_shift line 15
  2. theorem OAI.SevenEighths.GammaZeroDetector.gamma_shift_norm_lower line 28
  3. theorem OAI.SevenEighths.GammaZeroDetector.gamma_power_bound line 38
  4. theorem OAI.SevenEighths.GammaZeroDetector.gamma_rapid_bound line 54
  5. theorem OAI.SevenEighths.GammaZeroDetector.gamma_differentiableAt_right line 77
  6. def OAI.SevenEighths.GammaZeroDetector.cancelledKernel line 85
  7. def OAI.SevenEighths.GammaZeroDetector.literalKernel line 88
  8. theorem OAI.SevenEighths.GammaZeroDetector.cancelledKernel_eq_literal line 91
  9. theorem OAI.SevenEighths.GammaZeroDetector.cancelledKernel_at_zero line 98
  10. theorem OAI.SevenEighths.GammaZeroDetector.dslope_entire line 102
  11. theorem OAI.SevenEighths.GammaZeroDetector.cancelledKernel_differentiableAt line 107
  12. theorem OAI.SevenEighths.GammaZeroDetector.literalKernel_norm line 115
  13. theorem OAI.SevenEighths.GammaZeroDetector.cancelledKernel_large_height_bound line 119
  14. theorem OAI.SevenEighths.GammaZeroDetector.cancelledKernel_strip_bound line 156
  15. theorem OAI.SevenEighths.GammaZeroDetector.cancelledKernel_vertical_integrable line 185
  16. theorem OAI.SevenEighths.GammaZeroDetector.cancelledKernel_contour_shift line 201
  17. theorem OAI.SevenEighths.GammaZeroDetector.literal_contour_shift line 217
  18. theorem OAI.SevenEighths.GammaZeroDetector.gamma_negative_quarter_bound line 238
  19. theorem OAI.SevenEighths.GammaZeroDetector.literal_shifted_integral_bound line 261
  20. theorem OAI.SevenEighths.GammaZeroDetector.literal_detector_bound line 291
  21. def OAI.SevenEighths.GammaZeroDetector.cutoffSet line 309
  22. theorem OAI.SevenEighths.GammaZeroDetector.mem_cutoffSet line 312
  23. def OAI.SevenEighths.GammaZeroDetector.cutoffTerm line 325
  24. def OAI.SevenEighths.GammaZeroDetector.cutoff line 329
  25. theorem OAI.SevenEighths.GammaZeroDetector.cutoffTerm_zero line 332
  26. theorem OAI.SevenEighths.GammaZeroDetector.cutoffTerm_eq line 336
  27. theorem OAI.SevenEighths.GammaZeroDetector.cutoff_eq_tsum line 343
  28. theorem OAI.SevenEighths.GammaZeroDetector.cutoffTerm_entire line 357
  29. theorem OAI.SevenEighths.GammaZeroDetector.cutoff_entire line 370
  30. theorem OAI.SevenEighths.GammaZeroDetector.cutoffTerm_norm_le line 374
  31. theorem OAI.SevenEighths.GammaZeroDetector.cutoff_norm_le line 393
  32. theorem OAI.SevenEighths.GammaZeroDetector.original_right_growth line 405
  33. theorem OAI.SevenEighths.GammaZeroDetector.shifted_original_growth line 440
  34. def OAI.SevenEighths.GammaZeroDetector.detectorIntegrand line 458
  35. def OAI.SevenEighths.GammaZeroDetector.detectorIntegral line 461
  36. theorem OAI.SevenEighths.GammaZeroDetector.detector_contour_shift line 464
  37. theorem OAI.SevenEighths.GammaZeroDetector.detector_integral_bound line 480
  38. theorem OAI.SevenEighths.GammaZeroDetector.detector_integrable line 504
  39. theorem OAI.SevenEighths.GammaZeroDetector.detectorIntegral_contour_normalization line 532
  40. theorem OAI.SevenEighths.GammaZeroDetector.detector_power_bound line 543
  41. theorem OAI.SevenEighths.GammaZeroDetector.detector_uniform_small line 573