OAI/NumberTheory/PrimeGaps/ContourIntegrals.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LargePrimeGaps.integrable_schwartz_contourKernel line 23
  2. def OAI.LargePrimeGaps.kernelConstant line 38
  3. def OAI.LargePrimeGaps.kernelAbsoluteConstant line 42
  4. theorem OAI.LargePrimeGaps.kernelAbsoluteConstant_nonneg line 46
  5. theorem OAI.LargePrimeGaps.kernel_integral_on_error line 50
  6. theorem OAI.LargePrimeGaps.eulerGlobalMajorant_div_rpow_tendsto line 79
  7. def OAI.LargePrimeGaps.uniformCoreError line 115
  8. theorem OAI.LargePrimeGaps.uniformCoreError_tendsto line 119
  9. theorem OAI.LargePrimeGaps.integrable_pow_mul_schwartz_contourKernel line 135
  10. theorem OAI.LargePrimeGaps.norm_integral_norm_tail_le line 153
  11. theorem OAI.LargePrimeGaps.kernel_integral_tail_bound line 177
  12. theorem OAI.LargePrimeGaps.BombieriVinogradov_quantitative_PNT line 186
  13. theorem OAI.LargePrimeGaps.uniformEulerError_nonneg line 211
  14. theorem OAI.LargePrimeGaps.uniformCoreError_nonneg line 221
  15. theorem OAI.LargePrimeGaps.frequencyW_div_norm_sum_le line 228
  16. theorem OAI.LargePrimeGaps.tupleFourier_scaled_uniform_core_error line 240
  17. theorem OAI.LargePrimeGaps.integrable_schwartz_tupleFourier line 278
  18. theorem OAI.LargePrimeGaps.integral_core_tail_error line 289
  19. theorem OAI.LargePrimeGaps.tupleFourier_integral_uniform_error line 307
  20. def OAI.LargePrimeGaps.densityCutoff line 375
  21. def OAI.LargePrimeGaps.densityCoreExponent line 377
  22. theorem OAI.LargePrimeGaps.densityCoreExponent_pos line 379
  23. theorem OAI.LargePrimeGaps.densityCutoff_tendsto line 383
  24. theorem OAI.LargePrimeGaps.sqrt_core_rate line 387
  25. theorem OAI.LargePrimeGaps.sqrt_core_rate_tendsto line 397
  26. theorem OAI.LargePrimeGaps.sqrt_core_quarter_rate line 407
  27. theorem OAI.LargePrimeGaps.eventually_sqrt_core_le_quarter line 413
  28. theorem OAI.LargePrimeGaps.densityCutoff_neg_rpow line 424
  29. theorem OAI.LargePrimeGaps.eventually_density_core_scale line 442
  30. theorem OAI.LargePrimeGaps.eventually_nat_rate_le_index line 452
  31. theorem OAI.LargePrimeGaps.eventually_rate_densityCutoff_le_pow line 458
  32. theorem OAI.LargePrimeGaps.sqrt_pow_even line 466
  33. theorem OAI.LargePrimeGaps.scaled_polynomial_tail line 469
  34. theorem OAI.LargePrimeGaps.kernel_polynomial_tail line 477
  35. theorem OAI.LargePrimeGaps.tupleFourier_integral_uniform_asymptotic line 485