OAI/NumberTheory/EgyptianFractions/OddPrimorial.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem337.card_divisors_prime_finset_product line 8
2. def OAI.Problem337.oddPrimorial line 27

   Source documentation

   The product of the first r odd primes.

   def oddPrimorial (r : ℕ) : ℕ := ∏ i ∈ Finset.range r, Nat.nth Nat.Prime (i + 1)

3. lemma OAI.Problem337.oddPrimorial_pos line 29
4. lemma OAI.Problem337.oddPrimorial_odd line 34
5. lemma OAI.Problem337.oddPrimorial_divisors_card line 43
6. lemma OAI.Problem337.oddPrimorial_gt_one line 59
7. lemma OAI.Problem337.primePrefixProduct_succ_eq_two_mul_oddPrimorial line 67
8. lemma OAI.Problem337.oddPrimorial_le_primePrefixProduct line 72
9. lemma OAI.Problem337.eventually_log_log_oddPrimorial_le line 78

   Source documentation

   A deliberately coarse size bound suffices for the representation-counting argument.

   lemma eventually_log_log_oddPrimorial_le :
       ∀ᶠ r : ℕ in Filter.atTop,
         Real.log (Real.log (oddPrimorial r : ℝ)) ≤ 4 * Real.log (r : ℝ) := by
   …

   Mentions: OAI.Problem337.oddPrimorial

10. theorem OAI.Problem337.eventually_odd_primorial_supply line 106

    Source documentation

    A supply of odd integers with exponentially many divisors but short double logarithm.

    theorem eventually_odd_primorial_supply :
        ∀ᶠ r : ℕ in Filter.atTop, ∃ Q : ℕ,
          1 < Q ∧ Odd Q ∧ 2^r ≤ Q.divisors.card ∧
          Real.log (Real.log (Q : ℝ)) ≤ 4 * Real.log (r : ℝ) := by
    …