OAI/NumberTheory/PrimeGaps/FourierDerivatives.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LargePrimeGaps.tendsto_log_rpow_div_nat_rpow line 23
  2. theorem OAI.LargePrimeGaps.uniformEulerError_tendsto line 28
  3. theorem OAI.LargePrimeGaps.radianFourier_lineDeriv line 101
  4. theorem OAI.LargePrimeGaps.radianFourier_add line 111
  5. theorem OAI.LargePrimeGaps.radianFourier_const_mul line 115
  6. def OAI.LargePrimeGaps.laplaceLineDeriv line 120
  7. theorem OAI.LargePrimeGaps.radianFourier_laplaceLineDeriv line 123
  8. theorem OAI.LargePrimeGaps.laplaceLineDeriv_apply line 132
  9. theorem OAI.LargePrimeGaps.contDiff_signedLineDeriv line 153
  10. theorem OAI.LargePrimeGaps.laplaceLineDeriv_laplaceSchwartz line 158
  11. theorem OAI.LargePrimeGaps.sourceFourier_signedLineDeriv line 166
  12. def OAI.LargePrimeGaps.signedDirections line 174
  13. theorem OAI.LargePrimeGaps.signedDirections_compact line 178
  14. theorem OAI.LargePrimeGaps.signedDirections_smooth line 185
  15. theorem OAI.LargePrimeGaps.sourceFourier_signedDirections line 191
  16. theorem OAI.LargePrimeGaps.sourceFourier_derivative_inversion line 205
  17. def OAI.LargePrimeGaps.familyKernel line 218
  18. def OAI.LargePrimeGaps.normalizedZetaProduct line 221
  19. theorem OAI.LargePrimeGaps.familyKernel_fibers line 224
  20. theorem OAI.LargePrimeGaps.familyKernel_homogeneous line 234
  21. theorem OAI.LargePrimeGaps.eulerZetaProduct_factorization line 244
  22. theorem OAI.LargePrimeGaps.familyKernel_norm_polynomial line 254
  23. theorem OAI.LargePrimeGaps.normalizedZetaProduct_error line 276
  24. theorem OAI.LargePrimeGaps.eulerZeta_norm_contour_error line 299
  25. theorem OAI.LargePrimeGaps.eulerZetaProduct_scaled_factorization line 323
  26. theorem OAI.LargePrimeGaps.eulerZetaProduct_scaled_error line 341
  27. def OAI.LargePrimeGaps.eulerGlobalMajorant line 351
  28. theorem OAI.LargePrimeGaps.norm_eulerGlobal_le line 354
  29. theorem OAI.LargePrimeGaps.tupleFourier_scaled_factorization line 393
  30. theorem OAI.LargePrimeGaps.norm_mul_mul_sub_le line 419
  31. theorem OAI.LargePrimeGaps.tupleFourier_scaled_core_error line 436
  32. def OAI.LargePrimeGaps.contourKernel line 463
  33. theorem OAI.LargePrimeGaps.continuous_contourKernel line 466
  34. theorem OAI.LargePrimeGaps.contourKernel_norm_polynomial line 479
  35. theorem OAI.LargePrimeGaps.schwartz_integrable_polynomial_majorant line 489