OAI/NumberTheory/EgyptianFractions/SmallPrimeDivisors.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.divisor_card_small_primes_bound line 9

   Source documentation

   A number with only small prime factors has few divisors once its logarithm is bounded.

   theorem divisor_card_small_primes_bound (z W : ℝ) {n : ℕ} (hn : n ≠ 0)
       (hz : 0 ≤ z) (hnW : Real.log (n : ℝ) ≤ W)
       (hsmall : ∀ p ∈ n.primeFactors, (p : ℝ) ≤ z) :
       (n.divisors.card : ℝ) ≤ Real.exp (z * Real.log (1 + W / Real.log 2)) := by
   …

2. theorem OAI.Problem337.truncatedDivisorCount_pointwise_exp_bound line 55

   Source documentation

   Split the factor list at z and combine the small- and large-prime estimates.

   theorem truncatedDivisorCount_pointwise_exp_bound (X z W : ℝ) {n : ℕ} (hn : n ≠ 0)
       (hX : 1 < X) (hz : 1 < z) (hXW : Real.log X ≤ W)
       (hnW : Real.log (n : ℝ) ≤ W) :
       (truncatedDivisorCount X n : ℝ) ≤
         Real.exp (z * Real.log (1 + W / Real.log 2) +
           (1 + Real.log (W / Real.log X)) * Real.log X / Real.log z) := by
   …

   Mentions: OAI.Problem337.truncatedDivisorCount

3. theorem OAI.Problem337.truncatedDivisorCount_pointwise_log_bound line 116

   Source documentation

   Logarithmic version of the elementary small/large-prime split.

   theorem truncatedDivisorCount_pointwise_log_bound (X z W : ℝ) {n : ℕ} (hn : n ≠ 0)
       (hX : 1 < X) (hz : 1 < z) (hXW : Real.log X ≤ W)
       (hnW : Real.log (n : ℝ) ≤ W) :
       Real.log (truncatedDivisorCount X n : ℝ) ≤
         z * Real.log (1 + W / Real.log 2) +
           (1 + Real.log (W / Real.log X)) * Real.log X / Real.log z := by
   …

   Mentions: OAI.Problem337.truncatedDivisorCount