OAI/NumberTheory/PrimeGaps/CharacterErrors.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargePrimeGaps.primeCharacterPrefix line 27
  2. def OAI.LargePrimeGaps.primeCharacterError line 30
  3. theorem OAI.LargePrimeGaps.character_prefix_orthogonality line 33
  4. theorem OAI.LargePrimeGaps.character_error_orthogonality line 52
  5. theorem OAI.LargePrimeGaps.endpointClassError_le_character_sum line 70
  6. def OAI.LargePrimeGaps.characterMeanError line 88
  7. theorem OAI.LargePrimeGaps.characterMeanError_nonneg line 91
  8. theorem OAI.LargePrimeGaps.endpointError_le_characterMeanError line 95
  9. theorem OAI.LargePrimeGaps.endpointErrors_le_characterMeanErrors line 105
  10. theorem OAI.LargePrimeGaps.vonMangoldt_noncoprime_sum_le line 112
  11. theorem OAI.LargePrimeGaps.primitiveCharacter_eq_one_iff line 149
  12. theorem OAI.LargePrimeGaps.primeCharacterPrefix_primitive_difference line 158
  13. theorem OAI.LargePrimeGaps.primeCharacterError_primitive_difference line 186
  14. theorem OAI.LargePrimeGaps.primeCharacterError_le_primitive line 197
  15. theorem OAI.LargePrimeGaps.characterMeanError_le_primitive_average line 206
  16. def OAI.LargePrimeGaps.primitiveErrorMass line 225
  17. theorem OAI.LargePrimeGaps.primitiveErrorMass_nonneg line 229
  18. theorem OAI.LargePrimeGaps.induced_primitive_sum_le line 233
  19. theorem OAI.LargePrimeGaps.endpointError_le_primitive_conductors line 261
  20. theorem OAI.LargePrimeGaps.nat_le_card_divisors_mul_totient line 268
  21. theorem OAI.LargePrimeGaps.divisorMultiplicity_two line 278
  22. theorem OAI.LargePrimeGaps.sum_totient_reciprocal_le line 288
  23. theorem OAI.LargePrimeGaps.reciprocal_totient_divisor_sum_le line 298
  24. theorem OAI.LargePrimeGaps.endpointErrors_le_primitive_weighted_sum line 362
  25. def OAI.LargePrimeGaps.arithmeticCutoff line 383
  26. theorem OAI.LargePrimeGaps.arithmeticCutoff_apply line 386
  27. theorem OAI.LargePrimeGaps.vaughan_identity line 389
  28. def OAI.LargePrimeGaps.vaughanSecondCoefficient line 404
  29. theorem OAI.LargePrimeGaps.vaughanSecondCoefficient_eq line 408
  30. theorem OAI.LargePrimeGaps.vaughanSecondCoefficient_nonneg line 419
  31. theorem OAI.LargePrimeGaps.vaughanSecondCoefficient_le_log line 424
  32. theorem OAI.LargePrimeGaps.vaughanSecondCoefficient_zero_of_le line 433