OAI/NumberTheory/JointDickman/Amplification/TiltedAdditionTail.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.tilted_required_product line 14
2. theorem OAI.JointDickman.tilted_required_product_bound line 26

   Source documentation

   The odds correction is uniformly bounded for every allowed numeric addition; its squarefree product is in the actual coefficient range.

   theorem tilted_required_product_bound :
       ∀ᶠ B : ℕ in atTop, ∀ Z : Finset ℕ, Z ⊆ auxiliaryPrimes B →
         (∏ p ∈ Z, p : ℕ) ≤ Real.exp ((16/5 : ℝ)*B) →
         (∏ p ∈ Z, 1/(2*(p : ℝ)-1)) ≤
           Real.exp 1*((1/2 : ℝ)^Z.card/(∏ p ∈ Z, p : ℕ)) := by
   …

   Mentions: OAI.JointDickman.auxiliaryPrimes

3. theorem OAI.JointDickman.tilted_addition_regular_tail line 39

   Source documentation

   Regularity is retained inside the probability. No conditional probability or reciprocal of a regularity event occurs.

   theorem tilted_addition_regular_tail {B L k : ℕ} {τ C : ℝ}
       (A Z : Finset ℕ) (hZ : Z ⊆ auxiliaryPrimes B \ A)
       (hk : k ∈ Icc 1 L)
       (hprefix : Z ⊆ primePrefix B ((k : ℝ)/L) Z)
       {t : ℝ} (ht : 0 ≤ t) :
       (∑ 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) ≤
         (∏ p ∈ Z, 1/(2*(p : ℝ)-1))*
           Real.exp (t*((((k : ℝ)/L)/2+τ)*auxiliaryLogLength B-Z.card)+
             (Real.exp (-t)-1)*
               ∑ p ∈ ((auxiliaryPrimes B \ A) \ Z) ∩
   …

   Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.primePrefix, OAI.JointDickman.RegularPrimeSet, OAI.JointDickman.bernoulliSubsetMass, OAI.JointDickman.auxiliaryLogLength