OAI/NumberTheory/JointDickman/Arithmetic/PrimeProductTail.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.prime_reciprocal_product_fiber line 12

   Source documentation

   Fixing all but one prime leaves an interval of multiplicative width N/Y. The bound is uniform in the product r of the fixed primes.

   theorem prime_reciprocal_product_fiber : ∃ C : ℝ, 0 ≤ C ∧
       ∀ (P : Finset ℕ) (y Y N r : ℝ), 2 ≤ y → 0 < Y → Y ≤ N → 0 < r →
         (∀ p ∈ P, p.Prime ∧ y < (p:ℝ)) →
         (∑ p ∈ P.filter (fun p : ℕ => Y < r*(p:ℝ) ∧ r*(p:ℝ) ≤ N), 1/(p:ℝ)) ≤
           (Real.log (N/Y)+C)/Real.log y := by
   …

2. def OAI.JointDickman.reciprocalPrimeTupleTail line 40
3. theorem OAI.JointDickman.reciprocalPrimeTupleTail_fibers line 45
4. theorem OAI.JointDickman.reciprocalPrimeTupleTail_bound line 68

   Source documentation

   Repeated primes are allowed. Thus this also controls every fixed-cardinality term of the squarefree divisor expansion.

   theorem reciprocalPrimeTupleTail_bound : ∃ C : ℝ, 0 ≤ C ∧
       ∀ (P : Finset ℕ) (h : ℕ) (y Y N : ℝ), 2 ≤ y → 0 < Y → Y ≤ N →
         (∀ p ∈ P, p.Prime ∧ y < (p:ℝ)) →
         reciprocalPrimeTupleTail P (h+1) Y N ≤
           ((Real.log (N/Y)+C)/Real.log y)*(∑ p ∈ P, 1/(p:ℝ))^h := by
   …

   Mentions: OAI.JointDickman.reciprocalPrimeTupleTail