OAI/NumberTheory/PrimeGaps/VaughanBounds.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LargePrimeGaps.sequenceSize_le_of_norm_le line 29
  2. def OAI.LargePrimeGaps.vaughanFirstSequence line 40
  3. def OAI.LargePrimeGaps.vaughanSecondSequence line 43
  4. theorem OAI.LargePrimeGaps.vaughanFirstSequence_norm_le line 46
  5. theorem OAI.LargePrimeGaps.vaughanFirstSequence_size_le line 54
  6. theorem OAI.LargePrimeGaps.vaughanSecondSequence_norm_le line 59
  7. theorem OAI.LargePrimeGaps.vaughanSecondSequence_size_le line 65
  8. theorem OAI.LargePrimeGaps.vaughan_typeII_block_mean line 70
  9. theorem OAI.LargePrimeGaps.sum_Icc_one_eq_range_of_zero line 89
  10. theorem OAI.LargePrimeGaps.sum_range_filter_prefix line 102
  11. theorem OAI.LargePrimeGaps.arithmeticCharacterSum_convolution_triangular line 112
  12. theorem OAI.LargePrimeGaps.vaughan_typeII_exact line 143
  13. def OAI.LargePrimeGaps.arithmeticL1 line 158
  14. theorem OAI.LargePrimeGaps.arithmeticCharacterSum_le_l1 line 161
  15. theorem OAI.LargePrimeGaps.arithmeticL1_nonneg line 170
  16. theorem OAI.LargePrimeGaps.arithmeticL1_cutoff_le line 173
  17. theorem OAI.LargePrimeGaps.arithmeticCharacterSum_log_convolution_bound line 195
  18. theorem OAI.LargePrimeGaps.arithmeticCharacterSum_zeta_convolution_bound line 208
  19. theorem OAI.LargePrimeGaps.arithmeticCutoff_mul_support line 226
  20. theorem OAI.LargePrimeGaps.vaughanShortCoefficient_abs_le line 239
  21. theorem OAI.LargePrimeGaps.arithmeticCutoff_eq_of_support line 268
  22. theorem OAI.LargePrimeGaps.vonMangoldt_cutoff_l1 line 275
  23. theorem OAI.LargePrimeGaps.moebius_cutoff_l1 line 283
  24. theorem OAI.LargePrimeGaps.vaughanShortCoefficient_l1 line 291
  25. theorem OAI.LargePrimeGaps.primitive_vaughan_bound line 305
  26. def OAI.LargePrimeGaps.hyperbolaBlock line 333
  27. theorem OAI.LargePrimeGaps.hyperbolaBlock_eq_triangle line 338
  28. theorem OAI.LargePrimeGaps.sum_Ico_one_pow_two line 378
  29. theorem OAI.LargePrimeGaps.vaughan_hyperbolaBlock_mean line 388
  30. theorem OAI.LargePrimeGaps.hyperbolaBlock_extend line 414
  31. theorem OAI.LargePrimeGaps.arithmeticCharacterSum_convolution_dyadic line 429
  32. theorem OAI.LargePrimeGaps.vaughan_typeII_dyadic line 446