OAI/NumberTheory/JointDickman/Arithmetic/AdditionIntervalSieve.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.addition_product_interval_sieve line 14

   Source documentation

   The quarter-product probability on an interval is controlled by its relative length and the explicit sieve remainder, uniformly in the upper prime cutoff.

   theorem addition_product_interval_sieve
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput) :
       ∃ K : ℝ, 0 < K ∧ ∀ (P Z u v : ℕ) (Q : Finset ℕ) (X : ℝ),
         u ≤ v → 2 ≤ Z → 0 < X →
         (∀ p ∈ Q, p.Prime) → (∀ p ∈ Q, P < p) →
         (Nat.primesLE Z).filter (fun p => P < p) ⊆ Q →
         (∀ n ∈ Ico u v, X ≤ (n : ℝ)) →
         (∑ n ∈ Ico u v, primeProductMass Q (1 / 4) n) ≤
           K * (((v : ℝ) - u) / (X * Real.log Z)) + 2 * (Z + 1 : ℝ) * Z / X := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.primeProductMass