OAI/NumberTheory/PrimeGaps/EulerChoices.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LargePrimeGaps.eulerChoices_norm_tsum_le line 21
  2. theorem OAI.LargePrimeGaps.primeMonomial_norm_le_rpow line 41
  3. def OAI.LargePrimeGaps.primeChoiceWeight line 56
  4. theorem OAI.LargePrimeGaps.primeChoiceWeight_norm_bound line 60
  5. theorem OAI.LargePrimeGaps.prime_power_tsum_le_log_zeta line 78
  6. def OAI.LargePrimeGaps.primeAllowedWeight line 94
  7. theorem OAI.LargePrimeGaps.primeAllowedWeight_norm_le line 97
  8. theorem OAI.LargePrimeGaps.primeAllowedWeight_summable_norm line 112
  9. theorem OAI.LargePrimeGaps.primeEulerChoices_hasProd line 124
  10. theorem OAI.LargePrimeGaps.primeEulerChoices_norm_tsum_le line 138
  11. def OAI.LargePrimeGaps.choiceSubset line 158
  12. theorem OAI.LargePrimeGaps.choiceSubset_of_mem line 163
  13. theorem OAI.LargePrimeGaps.choiceSubset_of_not_mem line 167
  14. def OAI.LargePrimeGaps.choiceDivisors line 171
  15. theorem OAI.LargePrimeGaps.choiceDivisors_squarefree line 176
  16. theorem OAI.LargePrimeGaps.prime_dvd_choiceDivisors line 187
  17. def OAI.LargePrimeGaps.tuplePrimeSupport line 202
  18. theorem OAI.LargePrimeGaps.mem_tuplePrimeSupport line 206
  19. def OAI.LargePrimeGaps.tuplePrimeSubset line 218
  20. theorem OAI.LargePrimeGaps.mem_tuplePrimeSubset line 223
  21. theorem OAI.LargePrimeGaps.tuplePrimeSubset_nonempty_iff line 228
  22. theorem OAI.LargePrimeGaps.choiceSubset_mem_of_nonempty line 234
  23. theorem OAI.LargePrimeGaps.choice_primeSubset line 243
  24. theorem OAI.LargePrimeGaps.choice_primeSupport line 249
  25. theorem OAI.LargePrimeGaps.eulerChoices_ext line 262
  26. theorem OAI.LargePrimeGaps.choiceDivisors_injective line 288
  27. def OAI.LargePrimeGaps.AllowedDivisorTuple line 297
  28. def OAI.LargePrimeGaps.tupleChoices line 301
  29. theorem OAI.LargePrimeGaps.tupleChoices_subset line 307
  30. theorem OAI.LargePrimeGaps.choiceDivisors_tupleChoices line 318
  31. def OAI.LargePrimeGaps.choiceTuple line 328
  32. def OAI.LargePrimeGaps.primeChoicesEquivTuple line 334
  33. theorem OAI.LargePrimeGaps.choice_double_prod line 346
  34. theorem OAI.LargePrimeGaps.moebius_choiceDivisors line 361
  35. theorem OAI.LargePrimeGaps.moebius_choiceDivisors_prod line 374
  36. theorem OAI.LargePrimeGaps.choiceDivisors_log line 383
  37. theorem OAI.LargePrimeGaps.primeMonomial_as_product line 391
  38. theorem OAI.LargePrimeGaps.choiceMonomial_prod line 395
  39. def OAI.LargePrimeGaps.tuplePrimeDensity line 409
  40. def OAI.LargePrimeGaps.tupleFourierCoefficient line 412
  41. theorem OAI.LargePrimeGaps.choiceTerm_eq_tupleFourierCoefficient line 417
  42. theorem OAI.LargePrimeGaps.tupleFourier_summable_norm line 435
  43. theorem OAI.LargePrimeGaps.tupleFourier_hasProd line 445
  44. theorem OAI.LargePrimeGaps.tupleFourier_norm_tsum_le line 457
  45. theorem OAI.LargePrimeGaps.tupleFourier_eq_H_zeta line 469
  46. theorem OAI.LargePrimeGaps.prime_dvd_finset_lcm line 480
  47. theorem OAI.LargePrimeGaps.tuplePrimeSupport_eq_modulus line 490
  48. theorem OAI.LargePrimeGaps.tupleModulus_eq_primeSupport_prod line 503
  49. theorem OAI.LargePrimeGaps.tupleTotient_eq_primeSupport_prod line 512
  50. theorem OAI.LargePrimeGaps.tuplePrimeDensity_zero line 524
  51. theorem OAI.LargePrimeGaps.tuplePrimeDensity_one line 529