OAI/NumberTheory/JointDickman/Amplification/LowNumericAdditionBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.low_numeric_addition_class_bound line 14

   Source documentation

   This is the numeric sum before choosing the Rankin parameter. All progression and squarefree-product hypotheses have been discharged for the actual class. Its only analytic inputs are the cited upper sieve and Mertens.

   theorem low_numeric_addition_class_bound
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput)
       {κ g ε : ℝ} (hκ : 0 < κ) (hg : 0 < g) (hg1 : g < 1) (hε : 0 < ε) :
       ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop,
         ∀ (L k : ℕ) (τ C : ℝ) (e j b d : ℕ) (q W : ℝ),
           k ∈ Icc 1 L → g ≤ (k : ℝ)/L →
           0 < e → 0 < b → 0 < j → j ≤ auxiliaryCutoff B → e.Coprime j →
           (e*b : ℕ) ≤ Real.exp (κ*B) → 0 < q → q ≤ 1 → 2*(j : ℝ) ≤ W →
           (∑ Z ∈ lowNumericAdditionClass B L τ C e j b d W,
             (1/2 : ℝ)^d/((∏ p ∈ Z, p : ℕ) : ℝ)) ≤
             (((1/2 : ℝ)/q)^d*Real.exp (((((k : ℝ)/L)/2+τ)*auxiliaryLogLength B)*Real.log 2))*
   …

   Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.lowNumericAdditionClass, OAI.JointDickman.auxiliaryLogLength