OAI/NumberTheory/PrimeGaps/VaughanIdentity.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LargePrimeGaps.monotone_weighted_prefix_bound line 29
  2. theorem OAI.LargePrimeGaps.log_nat_monotone line 53
  3. theorem OAI.LargePrimeGaps.primitive_log_character_bound line 63
  4. theorem OAI.LargePrimeGaps.primitive_typeI_log_bound line 76
  5. theorem OAI.LargePrimeGaps.primitive_typeI_bound line 99
  6. def OAI.LargePrimeGaps.sequenceSize line 119
  7. theorem OAI.LargePrimeGaps.sequenceSize_nonneg line 122
  8. theorem OAI.LargePrimeGaps.sequenceSize_sq line 124
  9. def OAI.LargePrimeGaps.sequenceMask line 127
  10. theorem OAI.LargePrimeGaps.sequenceMask_size_le line 130
  11. theorem OAI.LargePrimeGaps.sequenceMask_size_partition line 138
  12. theorem OAI.LargePrimeGaps.sequenceMask_cauchy line 146
  13. def OAI.LargePrimeGaps.sieveBilinearConstant line 159
  14. theorem OAI.LargePrimeGaps.sieveBilinearConstant_nonneg line 163
  15. theorem OAI.LargePrimeGaps.bilinear_primitive_mean_le line 167
  16. theorem OAI.LargePrimeGaps.primitiveCharacterMean_mono line 189
  17. theorem OAI.LargePrimeGaps.primitiveCharacterMean_add line 196
  18. def OAI.LargePrimeGaps.triangularCharacterSum line 202
  19. theorem OAI.LargePrimeGaps.triangularCharacterSum_split line 206
  20. theorem OAI.LargePrimeGaps.triangularCharacterSum_single line 223
  21. theorem OAI.LargePrimeGaps.triangular_primitive_mean_dyadic line 239
  22. theorem OAI.LargePrimeGaps.triangular_primitive_mean_le line 300
  23. theorem OAI.LargePrimeGaps.sum_divisorsAntidiagonal_hyperbola line 308
  24. def OAI.LargePrimeGaps.arithmeticCharacterSum line 349
  25. theorem OAI.LargePrimeGaps.arithmeticCharacterSum_convolution line 353
  26. theorem OAI.LargePrimeGaps.arithmeticCharacterSum_add line 376
  27. theorem OAI.LargePrimeGaps.arithmeticCharacterSum_sub line 381
  28. theorem OAI.LargePrimeGaps.vaughan_character_identity line 392