OAI/NumberTheory/Jacobsthal/Sieve/EulerProductRatio.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.ErdosVarianceMoments.prime_residue_choices_card line 16
  2. theorem OAI.Erdos970.ErdosVarianceMoments.prime_unit_avoidance_card line 35
  3. theorem OAI.Erdos970.ErdosVarianceMoments.product_allowed_eq_density line 60
  4. def OAI.Erdos970.ErdosVarianceMoments.primeResidueSet line 82
  5. theorem OAI.Erdos970.ErdosVarianceMoments.primeResidueSet_card line 87
  6. theorem OAI.Erdos970.ErdosVarianceMoments.cast_int_residue line 93
  7. theorem OAI.Erdos970.ErdosVarianceMoments.int_mem_primeResidueSet line 98
  8. def OAI.Erdos970.ErdosVarianceMoments.integerPrimeIntersection line 107
  9. theorem OAI.Erdos970.ErdosVarianceMoments.integerPrimeIntersection_error line 111
  10. def OAI.Erdos970.NumberTheoryLean.RealFundamentalSieve.levelDivisors line 139
  11. theorem OAI.Erdos970.NumberTheoryLean.RealFundamentalSieve.floor_level_le line 143
  12. theorem OAI.Erdos970.NumberTheoryLean.RealFundamentalSieve.fundamental_lemma line 151
  13. def OAI.Erdos970.ErdosVarianceMoments.unitIntervalIntegers line 198
  14. def OAI.Erdos970.ErdosVarianceMoments.residueDensity line 201
  15. theorem OAI.Erdos970.ErdosVarianceMoments.actual_intersection_mass line 204
  16. theorem OAI.Erdos970.ErdosVarianceMoments.integerRemainder_bound line 219
  17. theorem OAI.Erdos970.ErdosVarianceMoments.remainder_sum_bound line 248
  18. def OAI.Erdos970.NumberTheoryLean.SmallSieveFinite.smallEuler line 295
  19. theorem OAI.Erdos970.NumberTheoryLean.SmallSieveFinite.squarefree_dvd_iff_primeFactors line 298
  20. theorem OAI.Erdos970.NumberTheoryLean.SmallSieveFinite.intersectionValue_divisibility line 310
  21. theorem OAI.Erdos970.NumberTheoryLean.SmallSieveFinite.reciprocal_primeFactors_product line 317
  22. theorem OAI.Erdos970.NumberTheoryLean.SmallSieveFinite.integerRemainder_eq_interval_rem line 321
  23. theorem OAI.Erdos970.NumberTheoryLean.SmallSieveFinite.integerRemainder_abs_le_two line 339
  24. theorem OAI.Erdos970.NumberTheoryLean.SmallSieveFinite.survives_sum_eq_coprimeOffsets line 359
  25. theorem OAI.Erdos970.NumberTheoryLean.SmallSieveFinite.realLevelDivisors_card_le line 377
  26. theorem OAI.Erdos970.NumberTheoryLean.SmallSieveFinite.cutoffSurvivors_eq_residueAvoidingOffsets line 390
  27. theorem OAI.Erdos970.NumberTheoryLean.SmallSieveFinite.finite_small_sieve_bound line 400
  28. theorem OAI.Erdos970.NumberTheoryLean.SmallSieveFinite.all_integer_euler_product line 439
  29. theorem OAI.Erdos970.NumberTheoryLean.SmallSieveFinite.smallEuler_ge_inv line 451
  30. theorem OAI.Erdos970.NumberTheoryLean.SmallSieveFinite.smallEuler_floor_ge_inv line 465
  31. theorem OAI.Erdos970.NumberTheoryLean.EulerProductRatio.restricted_block_union line 480
  32. theorem OAI.Erdos970.NumberTheoryLean.EulerProductRatio.tail_euler_lower line 505
  33. theorem OAI.Erdos970.NumberTheoryLean.EulerProductRatio.smallEuler_nonneg line 545
  34. theorem OAI.Erdos970.NumberTheoryLean.EulerProductRatio.smallEuler_ratio_nat line 552
  35. def OAI.Erdos970.NumberTheoryLean.EulerProductRatio.rootCutoff line 595
  36. theorem OAI.Erdos970.NumberTheoryLean.EulerProductRatio.rootExponent_pos line 597
  37. theorem OAI.Erdos970.NumberTheoryLean.EulerProductRatio.rootExponent_le_one line 599
  38. theorem OAI.Erdos970.NumberTheoryLean.EulerProductRatio.rootCutoff_le line 602
  39. theorem OAI.Erdos970.NumberTheoryLean.EulerProductRatio.rootCutoff_ge_two line 605
  40. theorem OAI.Erdos970.NumberTheoryLean.EulerProductRatio.geometric_endpoint_le_rootCutoff line 611
  41. theorem OAI.Erdos970.NumberTheoryLean.EulerProductRatio.smallEuler_ratio_rootCutoff line 634