OAI/NumberTheory/ShortEgyptian/PrimeProducts.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ShortEgyptian.prime_product_fiber_card line 13
  2. def OAI.ShortEgyptian.finiteMass line 41
  3. lemma OAI.ShortEgyptian.finiteMass_nonneg line 44
  4. lemma OAI.ShortEgyptian.finiteMass_sum line 47
  5. lemma OAI.ShortEgyptian.finiteMass_expect line 56
  6. lemma OAI.ShortEgyptian.prime_product_atom line 68
  7. lemma OAI.ShortEgyptian.prime_product_mod_atom line 77
  8. lemma OAI.ShortEgyptian.expect_prod_pi line 93
  9. lemma OAI.ShortEgyptian.finiteMass_indicator line 100
  10. lemma OAI.ShortEgyptian.finite_markov line 105
  11. lemma OAI.ShortEgyptian.finite_union_bound line 116
  12. lemma OAI.ShortEgyptian.gcd_prod_le_hits line 127
  13. lemma OAI.ShortEgyptian.gcd_product_moment line 146
  14. lemma OAI.ShortEgyptian.prime_divisor_count line 186
  15. lemma OAI.ShortEgyptian.prime_hit_probability line 198
  16. lemma OAI.ShortEgyptian.uniform_prime_bilinear line 213
  17. lemma OAI.ShortEgyptian.expect_pi_split line 236
  18. lemma OAI.ShortEgyptian.expect_restrict_subtype line 250
  19. lemma OAI.ShortEgyptian.expect_restrict_injective line 262