OAI/NumberTheory/EgyptianFractions/PrimeProductBound.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Problem337.primeCounting_nth_prime line 10
  2. lemma OAI.Problem337.nth_prime_chebyshev_bound line 14
  3. lemma OAI.Problem337.tendsto_nth_prime_atTop line 35
  4. lemma OAI.Problem337.eventually_log_nth_prime_le line 42
  5. def OAI.Problem337.primePrefixProduct line 94

    Source documentation

    Product of the first n primes, indexed from zero.

    def primePrefixProduct (n : ℕ) : ℕ := ∏ i ∈ Finset.range n, Nat.nth Nat.Prime i
  6. lemma OAI.Problem337.primePrefixProduct_pos line 96
  7. lemma OAI.Problem337.primePrefixProduct_dvd_mono line 101
  8. lemma OAI.Problem337.two_pow_le_primePrefixProduct line 105
  9. lemma OAI.Problem337.log_primePrefixProduct_le line 113
  10. lemma OAI.Problem337.eventually_log_primePrefixProduct_le line 131
  11. lemma OAI.Problem337.card_divisors_primePrefixProduct line 142