OAI/NumberTheory/Jacobsthal/Primes/GuardedHardPrimeSets.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.ErdosVarianceWeighted.subset_card_of_fraction line 17
  2. theorem OAI.Erdos970.ErdosVarianceWeighted.harmonic_transfer line 26
  3. theorem OAI.Erdos970.ErdosVarianceWeighted.harmonic_transfer_two line 54
  4. def OAI.Erdos970.ErdosVarianceUniformMoments.modelBadEvent line 75
  5. theorem OAI.Erdos970.ErdosVarianceUniformMoments.uniform_model_chebyshev line 81
  6. theorem OAI.Erdos970.ErdosVarianceSmallPrime.common_deviation_mem_primeEvent line 129
  7. def OAI.Erdos970.ErdosVarianceSmallPrime.badAligningPrimes line 157
  8. theorem OAI.Erdos970.ErdosVarianceSmallPrime.mem_badAligningPrimes line 163
  9. def OAI.Erdos970.ErdosVarianceLargePrime.fullPatternBadEvent line 179
  10. theorem OAI.Erdos970.ErdosVarianceLargePrime.common_deviation_mem_full_event line 185
  11. theorem OAI.Erdos970.ErdosVarianceSmallPrime.source_small_H_bad_prime_fraction line 219
  12. theorem OAI.Erdos970.ErdosVarianceLargePrime.source_large_H_bad_prime_fraction line 313
  13. theorem OAI.Erdos970.ErdosVarianceLargePrime.source_hard_bad_prime_fraction line 401
  14. def OAI.Erdos970.ErdosVarianceWeighted.hardCandidate line 444
  15. def OAI.Erdos970.ErdosVarianceWeighted.guardedHardPrimes line 449
  16. def OAI.Erdos970.ErdosVarianceWeighted.rawHardPrimeUnion line 453
  17. theorem OAI.Erdos970.ErdosVarianceWeighted.guardedHardPrimes_subset line 456
  18. theorem OAI.Erdos970.ErdosVarianceWeighted.rawHardPrimeUnion_subset line 463
  19. theorem OAI.Erdos970.ErdosVarianceWeighted.mem_rawHardPrimeUnion line 467
  20. theorem OAI.Erdos970.ErdosVarianceWeighted.rawHardPrimeUnion_card line 478