OAI/NumberTheory/EgyptianFractions/LargePrimeDivisors.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.truncatedDivisorCount_le_binomial_of_length line 10

   Source documentation

   Counting prime-factor sublists, with multiplicities labeled, overcounts divisors.

   theorem truncatedDivisorCount_le_binomial_of_length (X t : ℝ) {n : ℕ} (hn : n ≠ 0)
       (hlen : ∀ a ∈ n.divisors, (a : ℝ) ≤ X → (a.primeFactorsList.length : ℝ) ≤ t) :
       truncatedDivisorCount X n ≤
         ∑ j ∈ (Finset.range (n.primeFactorsList.length + 1)).filter
             (fun j : ℕ => (j : ℝ) ≤ t), Nat.choose n.primeFactorsList.length j := by
   …

   Mentions: OAI.Problem337.truncatedDivisorCount

2. theorem OAI.Problem337.pow_length_le_nat_list_prod line 42
3. theorem OAI.Problem337.primeFactorsList_length_le_log line 53

   Source documentation

   If all prime factors are at least z, their number is bounded by log n / log z.

   theorem primeFactorsList_length_le_log {n : ℕ} (hn : n ≠ 0) {z : ℝ} (hz : 1 < z)
       (hlarge : ∀ p ∈ n.primeFactorsList, z ≤ (p : ℝ)) :
       (n.primeFactorsList.length : ℝ) ≤ Real.log (n : ℝ) / Real.log z := by
   …

4. theorem OAI.Problem337.truncatedDivisorCount_large_primes_exp line 63

   Source documentation

   Large prime factors give the standard weighted-binomial divisor bound.

   theorem truncatedDivisorCount_large_primes_exp (X z q : ℝ) {n : ℕ} (hn : n ≠ 0)
       (hz : 1 < z) (hq0 : 0 < q) (hq1 : q ≤ 1)
       (hlarge : ∀ p ∈ n.primeFactorsList, z ≤ (p : ℝ)) :
       (truncatedDivisorCount X n : ℝ) ≤
         Real.exp (-(Real.log X / Real.log z) * Real.log q +
           (n.primeFactorsList.length : ℝ) * q) := by
   …

   Mentions: OAI.Problem337.truncatedDivisorCount

5. theorem OAI.Problem337.truncatedDivisorCount_large_primes_bound line 83

   Source documentation

   The large-prime divisor estimate in the entropy form used by the manuscript.

   theorem truncatedDivisorCount_large_primes_bound (X z W : ℝ) {n : ℕ} (hn : n ≠ 0)
       (hX : 1 < X) (hz : 1 < z) (hXW : Real.log X ≤ W)
       (hnW : Real.log (n : ℝ) ≤ W)
       (hlarge : ∀ p ∈ n.primeFactorsList, z ≤ (p : ℝ)) :
       (truncatedDivisorCount X n : ℝ) ≤
         Real.exp ((1 + Real.log (W / Real.log X)) * Real.log X / Real.log z) := by
   …

   Mentions: OAI.Problem337.truncatedDivisorCount

6. theorem OAI.Problem337.truncatedDivisorCount_prefix_moment_bound line 111

   Source documentation

   Splitting off any prefix of the factorization gives the divisor-prefix moment bound.

   theorem truncatedDivisorCount_prefix_moment_bound (X z W r : ℝ) {n d : ℕ}
       (hn : n ≠ 0) (hd : d ∣ n) (hX : 1 < X) (hz : 1 < z)
       (hXW : Real.log X ≤ W) (hnW : Real.log (n : ℝ) ≤ W) (hr : 0 ≤ r)
       (hlarge : ∀ p ∈ (n / d).primeFactorsList, z ≤ (p : ℝ)) :
       (truncatedDivisorCount X n : ℝ) ^ r ≤ (d.divisors.card : ℝ) ^ r *
         Real.exp (r * ((1 + Real.log (W / Real.log X)) * Real.log X / Real.log z)) := by
   …

   Mentions: OAI.Problem337.truncatedDivisorCount