OAI/NumberTheory/JointDickman/Amplification/TiltedAdditionRate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.clippedAdditionDensity line 13
2. theorem OAI.JointDickman.tilted_addition_rate_bound line 18

   Source documentation

   Both the inclusion cost and the lower-tail cost are present. The first remainder's regularity is inside the probability, as in (27) of moments.tex.

   theorem tilted_addition_rate_bound
       (hM : PublishedInputs.PrimeReciprocalMertensInput)
       {L k : ℕ} (hk : k ∈ Icc 1 L) {τ δ ε : ℝ} (hτ : 0 ≤ τ)
       (hδ : 0 < δ) (hδ1 : δ ≤ 1/2) (hε : 0 < ε) :
       ∀ᶠ B : ℕ in atTop, ∀ (C : ℝ) (A Z : Finset ℕ),
         A ⊆ auxiliaryPrimes B → Z ⊆ auxiliaryPrimes B \ A →
         (∏ p ∈ A, p : ℕ) ≤ Real.exp ((16/5 : ℝ)*B) →
         (∏ p ∈ Z, p : ℕ) ≤ Real.exp ((16/5 : ℝ)*B) →
         Z ⊆ primePrefix B ((k : ℝ)/L) Z →
         (∑ R ∈ (auxiliaryPrimes B \ A).powerset,
           if Z ⊆ R ∧ RegularPrimeSet B L τ C R then
             bernoulliSubsetMass (auxiliaryPrimes B \ A) (fun p => 1/(2*(p : ℝ)-1)) R else 0) ≤
   …

   Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.primePrefix, OAI.JointDickman.RegularPrimeSet, OAI.JointDickman.bernoulliSubsetMass