OAI/NumberTheory/PowerFree/Sieve.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuarticPowerFree.resultant_derivative_ne_zero line 11
  2. theorem OAI.QuarticPowerFree.derivative_not_dvd_of_good line 24
  3. theorem OAI.QuarticPowerFree.divided_difference_eval line 36
  4. theorem OAI.QuarticPowerFree.eval_sub_eq_mul_divided_difference line 43
  5. theorem OAI.QuarticPowerFree.prime_power_root_unique line 50
  6. theorem OAI.QuarticPowerFree.map_zmod_ne_zero_of_good line 69
  7. theorem OAI.QuarticPowerFree.rho_prime_pow_le_degree line 84
  8. theorem OAI.QuarticPowerFree.finite_resultant_primes line 133
  9. theorem OAI.QuarticPowerFree.summable_local_proportion line 146
  10. theorem OAI.QuarticPowerFree.localFactor_pos line 161
  11. theorem OAI.QuarticPowerFree.densityConstant_converges_pos line 168
  12. theorem OAI.QuarticPowerFree.count_mul_periodic line 183
  13. theorem OAI.QuarticPowerFree.count_periodic_div_mod line 196
  14. theorem OAI.QuarticPowerFree.count_periodic_error line 206
  15. theorem OAI.QuarticPowerFree.count_residues line 233
  16. theorem OAI.QuarticPowerFree.count_crt line 251
  17. def OAI.QuarticPowerFree.AvoidPrimes line 278
  18. instance OAI.QuarticPowerFree.(instance at line 281) line 281
  19. theorem OAI.QuarticPowerFree.eval_zmod_eq_zero_iff line 285
  20. theorem OAI.QuarticPowerFree.rho_le line 294
  21. theorem OAI.QuarticPowerFree.card_good_residues line 297
  22. theorem OAI.QuarticPowerFree.finite_sieve_full_period line 304
  23. theorem OAI.QuarticPowerFree.finite_sieve_periodic line 331
  24. theorem OAI.QuarticPowerFree.finite_sieve_error line 350
  25. theorem OAI.QuarticPowerFree.count_or_le line 371
  26. theorem OAI.QuarticPowerFree.count_exists_le line 376
  27. theorem OAI.QuarticPowerFree.root_predicate_periodic line 386
  28. theorem OAI.QuarticPowerFree.count_roots_le line 394
  29. def OAI.QuarticPowerFree.primesUpTo line 411
  30. theorem OAI.QuarticPowerFree.mem_primesUpTo line 413
  31. theorem OAI.QuarticPowerFree.card_primesUpTo line 418
  32. theorem OAI.QuarticPowerFree.primeCounting_ratio_tendsto line 425
  33. theorem OAI.QuarticPowerFree.tendsto_primesUpTo line 442
  34. theorem OAI.QuarticPowerFree.finite_product_tendsto line 449
  35. theorem OAI.QuarticPowerFree.finite_local_tail_small line 455
  36. def OAI.QuarticPowerFree.natCount line 471
  37. def OAI.QuarticPowerFree.tailCount line 475
  38. theorem OAI.QuarticPowerFree.natCount_le_finite line 480
  39. theorem OAI.QuarticPowerFree.finite_sieve_difference_le line 487
  40. theorem OAI.QuarticPowerFree.intermediate_sieve_bound line 516
  41. theorem OAI.QuarticPowerFree.finite_sieve_ratio_tendsto line 552
  42. theorem OAI.QuarticPowerFree.exists_bad_prime_cutoff line 570
  43. theorem OAI.QuarticPowerFree.finite_ratio_difference_le line 579
  44. theorem OAI.QuarticPowerFree.nat_density_from_large_prime_tail line 603
  45. theorem OAI.QuarticPowerFree.count_interval_compare line 648
  46. theorem OAI.QuarticPowerFree.count_natCount_error line 676
  47. theorem OAI.QuarticPowerFree.real_asymptotic_from_nat_ratio line 691
  48. theorem OAI.QuarticPowerFree.densityStatement_from_large_prime_tail line 730
  49. theorem OAI.QuarticPowerFree.linear_envelope_of_halving line 739
  50. theorem OAI.QuarticPowerFree.tendsto_zero_of_halving line 763
  51. def OAI.QuarticPowerFree.dyadicTailCount line 799
  52. theorem OAI.QuarticPowerFree.tailCount_halving line 804
  53. theorem OAI.QuarticPowerFree.global_tail_of_dyadic_tail line 832
  54. theorem OAI.QuarticPowerFree.exists_primitive_positive_normalization line 849
  55. theorem OAI.QuarticPowerFree.prime_power_dvd_scalar_iff line 878
  56. theorem OAI.QuarticPowerFree.tailCount_scalar_eq line 886
  57. theorem OAI.QuarticPowerFree.global_tail_scalar_iff line 902
  58. theorem OAI.QuarticPowerFree.dyadic_tail_limit_of_power_saving line 909
  59. theorem OAI.QuarticPowerFree.densityStatement_from_normalized_dyadic_tail line 926