OAI/NumberTheory/JointDickman/Probability/OrientedSplitBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.additionRatioTest line 13
2. def OAI.JointDickman.orientedSplitMass line 18
3. theorem OAI.JointDickman.additionRatioTest_average line 29
4. theorem OAI.JointDickman.oriented_split_bound line 44

   Source documentation

   The no-high-change probability and the low ratio probability multiply in the exact conditional law. This statement retains the actual high masses.

   theorem oriented_split_bound
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput) (κ : ℝ) :
       ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop, ∀ (A D : Finset ℕ) (Y C T : ℝ),
         A ⊆ auxiliaryPrimes B → D ⊆ auxiliaryPrimes B →
         (∏ p ∈ A, p : ℕ) ≤ Real.exp (κ * B) →
         0 < Y → Real.log (auxiliaryCutoff B) ≤ Y → Y ≤ 8 * B → 0 < T →
         orientedSplitMass B A D Y C T ≤
           (1 / 2 : ℝ)^(A ∩ upperAdditionPrimes B Y).card *
           (1 / 2 : ℝ)^(D ∩ upperAdditionPrimes B Y).card *
           (highNoAdditionMass (upperAdditionPrimes B Y) (remainingPrimeParameter D)
             ((2 / 5 : ℝ) * Real.log ((B : ℝ) / Y) - C) *
   …

   Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.orientedSplitMass, OAI.JointDickman.upperAdditionPrimes, OAI.JointDickman.highNoAdditionMass, OAI.JointDickman.remainingPrimeParameter