OAI/NumberTheory/JointDickman/Arithmetic/RegularityPrimeSums.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.auxiliaryCutoff_le_exp_rpow line 13
2. theorem OAI.JointDickman.regularity_prefix_prime_sum_tendsto line 35

   Source documentation

   Both interior prefixes and the full fixed exponential cutoff have normalized reciprocal-prime mass g; the endpoint multiplier c contributes only a bounded logarithm.

   theorem regularity_prefix_prime_sum_tendsto
       (hM : PublishedInputs.PrimeReciprocalMertensInput) {c g : ℝ}
       (hc : 0 < c) (hg : 0 < g) :
       Tendsto (fun B : ℕ =>
         (∑ p ∈ largePrimeSet (Real.exp (c * (B : ℝ) ^ g)) (auxiliaryCutoff B), 1 / (p : ℝ)) /
           auxiliaryLogLength B) atTop (𝓝 g) := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.largePrimeSet, OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.auxiliaryLogLength