OAI/NumberTheory/PrimeGaps/ContourSums.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargePrimeGaps.fourierCoordinateSum line 23
  2. theorem OAI.LargePrimeGaps.fourierCoordinateSum_apply line 26
  3. def OAI.LargePrimeGaps.divisorLogVector line 29
  4. theorem OAI.LargePrimeGaps.divisorLogVector_apply line 32
  5. def OAI.LargePrimeGaps.fourierContour line 35
  6. theorem OAI.LargePrimeGaps.fourierContour_re line 38
  7. theorem OAI.LargePrimeGaps.tupleFourierCoefficient_norm_eq_of_re line 42
  8. theorem OAI.LargePrimeGaps.tupleFourierCoefficient_contour_norm line 49
  9. theorem OAI.LargePrimeGaps.continuous_tupleFourierCoefficient_contour line 57
  10. theorem OAI.LargePrimeGaps.contour_sum_log_eq line 63
  11. theorem OAI.LargePrimeGaps.integral_sourceFourier_tupleCoefficient line 76
  12. theorem OAI.LargePrimeGaps.integrable_sourceFourier_tupleCoefficient line 91
  13. def OAI.LargePrimeGaps.analyticDensity line 98
  14. theorem OAI.LargePrimeGaps.analyticDensity_eq_integral line 104
  15. theorem OAI.LargePrimeGaps.allowed_residue_iff line 130
  16. theorem OAI.LargePrimeGaps.allowed_marked_residue_iff line 150
  17. theorem OAI.LargePrimeGaps.analyticDensity_eq_unmarked_tsum line 179
  18. theorem OAI.LargePrimeGaps.analyticDensity_eq_marked_tsum line 214
  19. theorem OAI.LargePrimeGaps.divisorCoefficient_support line 249
  20. theorem OAI.LargePrimeGaps.analyticDensity_eq_unmarkedDensitySum line 260
  21. theorem OAI.LargePrimeGaps.analyticDensity_eq_markedDensitySum line 272
  22. theorem OAI.LargePrimeGaps.schwartz_integral_tail_bound line 285
  23. theorem OAI.LargePrimeGaps.continuous_tupleFourier_tsum line 315
  24. theorem OAI.LargePrimeGaps.tupleFourier_tsum_norm_bound line 327
  25. theorem OAI.LargePrimeGaps.tupleFourier_schwartz_tail line 337
  26. theorem OAI.LargePrimeGaps.zeta_contour_majorant_polynomial line 350
  27. theorem OAI.LargePrimeGaps.tupleFourier_sqrt_tail_power_saving line 377
  28. theorem OAI.LargePrimeGaps.nonemptySubsets_singleton line 405
  29. theorem OAI.LargePrimeGaps.nonemptySubsets_pair line 412
  30. theorem OAI.LargePrimeGaps.fiberKernel_singleton line 427
  31. theorem OAI.LargePrimeGaps.fiberKernel_pair line 431
  32. theorem OAI.LargePrimeGaps.integral_exp_neg_complex_Ioi line 440
  33. theorem OAI.LargePrimeGaps.fiberKernel_pair_laplace line 444
  34. theorem OAI.LargePrimeGaps.primeReciprocalPrefix_eq line 452
  35. theorem OAI.LargePrimeGaps.genericEulerConstant_mono line 457
  36. theorem OAI.LargePrimeGaps.primeReciprocalPrefix_nonneg line 463
  37. theorem OAI.LargePrimeGaps.exp_sub_one_le_two_mul line 467
  38. def OAI.LargePrimeGaps.uniformEulerError line 474
  39. theorem OAI.LargePrimeGaps.eulerGlobal_uniform_error line 479