OAI/NumberTheory/JointDickman/Amplification/LargeLowAdditionAvailability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.availableLowNumericAdditionClass line 12
2. theorem OAI.JointDickman.large_low_addition_availability_bound line 22

   Source documentation

   The Poisson penalty in the first remainder and the numeric Rankin exponent cancel to half the binary entropy, as in equations (27)--(29). The expectation keeps the first remainder's full regularity condition.

   theorem large_low_addition_availability_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 ≤ τ) (hτ1 : τ ≤ 1) (hε : 0 < ε) :
       ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop,
         ∀ (C : ℝ) (A : Finset ℕ) (e j b d : ℕ) (W : ℝ),
           A ⊆ auxiliaryPrimes B → (∏ p ∈ A, p : ℕ) ≤ Real.exp ((16/5 : ℝ)*B) →
           0 < e → 0 < b → 0 < j → j ≤ auxiliaryCutoff B → e.Coprime j →
           (e*b : ℕ) ≤ Real.exp (κ*B) → (j : ℝ) ≤ (B : ℝ)^2 →
   …

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