OAI/NumberTheory/JointDickman/Counting/AdditionRatioWindow.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.ratio_log_bounds line 12
2. theorem OAI.JointDickman.first_addition_log_window line 23
3. theorem OAI.JointDickman.second_addition_log_window line 33
4. def OAI.JointDickman.firstAdditionRatioMass line 44
5. theorem OAI.JointDickman.first_addition_ratio_bound line 55

   Source documentation

   Uniformly in both retained coefficient products, an oriented second-ratio event has conditional mass O(1/Y).

   theorem first_addition_ratio_bound
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput) (κ : ℝ) :
       ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop, ∀ (A D : Finset ℕ) (Y T a c : ℝ),
         A ⊆ auxiliaryPrimes B → (∏ p ∈ A, p : ℕ) ≤ Real.exp (κ * B) →
         Real.log (auxiliaryCutoff B) ≤ Y → Y ≤ 8 * B → 0 < T → 0 < a → 0 < c →
         firstAdditionRatioMass B A D Y T a c ≤ K / Y := by
   …

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