OAI/NumberTheory/DirichletL/GammaDetectorExpansion.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.GammaDetectorExpansion.line line 13
  2. theorem OAI.SevenEighths.GammaDetectorExpansion.line_re line 15
  3. theorem OAI.SevenEighths.GammaDetectorExpansion.line_im line 16
  4. theorem OAI.SevenEighths.GammaDetectorExpansion.gamma_line_integrable line 18
  5. theorem OAI.SevenEighths.GammaDetectorExpansion.gamma_mellin_inverse line 33
  6. def OAI.SevenEighths.GammaDetectorExpansion.gammaTerm line 52
  7. theorem OAI.SevenEighths.GammaDetectorExpansion.gammaTerm_separate line 55
  8. theorem OAI.SevenEighths.GammaDetectorExpansion.gammaTerm_integral line 63
  9. theorem OAI.SevenEighths.GammaDetectorExpansion.gammaTerm_zero line 73
  10. theorem OAI.SevenEighths.GammaDetectorExpansion.gammaTerm_norm line 76
  11. theorem OAI.SevenEighths.GammaDetectorExpansion.gammaTerm_integrable line 83
  12. theorem OAI.SevenEighths.GammaDetectorExpansion.gamma_expansion line 98
  13. instance OAI.SevenEighths.GammaDetectorExpansion.(instance at line 131) line 131
  14. instance OAI.SevenEighths.GammaDetectorExpansion.(instance at line 132) line 132
  15. theorem OAI.SevenEighths.GammaDetectorExpansion.cutoffTerm_weighted line 134
  16. theorem OAI.SevenEighths.GammaDetectorExpansion.cutoffTerm_outside line 141
  17. theorem OAI.SevenEighths.GammaDetectorExpansion.cutoffTerm_hasSum line 152
  18. def OAI.SevenEighths.GammaDetectorExpansion.pairCoefficient line 157
  19. def OAI.SevenEighths.GammaDetectorExpansion.pairNorm line 161
  20. theorem OAI.SevenEighths.GammaDetectorExpansion.pairCoefficient_zero_norm line 163
  21. theorem OAI.SevenEighths.GammaDetectorExpansion.pairTerm_eq line 170
  22. theorem OAI.SevenEighths.GammaDetectorExpansion.pairTerm_summable_norm line 185
  23. theorem OAI.SevenEighths.GammaDetectorExpansion.pairSeries_eq line 193
  24. theorem OAI.SevenEighths.GammaDetectorExpansion.pairMajorant_summable line 203
  25. theorem OAI.SevenEighths.GammaDetectorExpansion.pairGamma_tsum line 217
  26. def OAI.SevenEighths.GammaDetectorExpansion.pairExponential line 233
  27. theorem OAI.SevenEighths.GammaDetectorExpansion.detector_hasSum_pairs line 237
  28. theorem OAI.SevenEighths.GammaDetectorExpansion.detector_eq_double_sum line 247
  29. theorem OAI.SevenEighths.GammaDetectorExpansion.pairExponential_zero_left line 258
  30. theorem OAI.SevenEighths.GammaDetectorExpansion.pairExponential_zero_right line 263
  31. theorem OAI.SevenEighths.GammaDetectorExpansion.pairExponential_fiber line 268
  32. theorem OAI.SevenEighths.GammaDetectorExpansion.detector_hasSum_convolution line 285
  33. theorem OAI.SevenEighths.GammaDetectorExpansion.detector_large_product_tail line 296
  34. theorem OAI.SevenEighths.GammaDetectorExpansion.pairExponential_summable_norm line 307
  35. def OAI.SevenEighths.GammaDetectorExpansion.pairTail line 313
  36. theorem OAI.SevenEighths.GammaDetectorExpansion.pairTail_summable line 317
  37. theorem OAI.SevenEighths.GammaDetectorExpansion.pairTail_fiber line 331
  38. theorem OAI.SevenEighths.GammaDetectorExpansion.detector_eq_pair_tail line 341