OAI/NumberTheory/JointDickman/Counting/CoefficientDomination.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.primeProductMass_coefficient_domination line 15

   Source documentation

   The actual prime-product probability is bounded by A₀(n)/(Bn), uniformly over the full product range needed by the application.

   theorem primeProductMass_coefficient_domination
       (hM : PublishedInputs.PrimeReciprocalMertensInput) :
       ∃ C : ℝ, 0 < C ∧ ∀ᶠ B : ℕ in atTop, ∀ n : ℕ, 0 < n →
         (n : ℝ) ≤ Real.exp ((16 / 5 : ℝ) * B) →
         primeProductMass (auxiliaryPrimes B) (1 / 2) n ≤
           C * coefficientWeight B n / ((B : ℝ) * n) := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.primeProductMass, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.coefficientWeight