OAI/NumberTheory/JointDickman/Amplification/AdditionSmallBall.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.addition_product_small_ball line 16

   Source documentation

   Any logarithmic interval of bounded length above Y/2 carries O(1/Y) quarter-product mass. The prime set may extend above or below the interval; only its containing the fixed sieve range is needed.

   theorem addition_product_small_ball
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput) {H : ℝ} (hH : 0 ≤ H) :
       ∃ K : ℝ, 0 < K ∧ ∀ᶠ Y : ℝ in atTop, ∀ (P : ℕ) (Q : Finset ℕ) (v : ℝ),
         Y / 2 ≤ v → (∀ p ∈ Q, p.Prime) → (∀ p ∈ Q, P < p) →
         (Nat.primesLE (additionSieveCutoff Y)).filter (fun p => P < p) ⊆ Q →
         (∑ n ∈ Icc ⌈Real.exp v⌉₊ ⌊Real.exp (v + H)⌋₊, primeProductMass Q (1 / 4) n) ≤ K / Y := by
   …

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