OAI/NumberTheory/JointDickman/Amplification/LargeLowNumericAddition.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.large_low_numeric_addition_bound line 17

   Source documentation

   Equation (28) of the manuscript, for a positive lag and the designated large addition at its low endpoint. The explicit sieve remainder has been absorbed uniformly in the cardinality class.

   theorem large_low_numeric_addition_bound
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput)
       {L k : ℕ} (hk : k ∈ Icc 1 L) {g κ Δ δ ε : ℝ}
       (hkg : (k : ℝ)/L = g) (hg : 0 < g) (hg1 : g ≤ 1)
       (hκ : 0 < κ) (hΔ : 0 < Δ) (hgap : 2*Δ < g)
       (hδ : 0 < δ) (hδ1 : δ ≤ 1/2) (hε : 0 < ε) :
       ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop,
         ∀ (τ C : ℝ) (e j b d : ℕ) (W : ℝ), 0 ≤ τ → τ ≤ 1 →
           0 < e → 0 < b → 0 < j → j ≤ auxiliaryCutoff B → e.Coprime j →
           (e*b : ℕ) ≤ Real.exp (κ*B) → (j : ℝ) ≤ (B : ℝ)^2 →
           2*(j : ℝ) ≤ W → Real.exp ((B : ℝ)^(g-Δ))/4 ≤ W →
   …

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