OAI/NumberTheory/JointDickman/Amplification/AuxiliaryScale.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The manuscript's auxiliary prime scale

The lower cutoff is B^1000, the upper cutoff is exp (4 B), and R = B / log (B^1000). The normalizing constant below is derived from the published reciprocal-prime Mertens estimate.

  1. def OAI.JointDickman.auxiliaryCutoff line 19
  2. def OAI.JointDickman.auxiliaryUpper line 21
  3. def OAI.JointDickman.auxiliaryRatio line 23
  4. def OAI.JointDickman.auxiliaryPrimes line 26
  5. theorem OAI.JointDickman.auxiliaryCutoff_tendsto line 29
  6. theorem OAI.JointDickman.auxiliaryUpper_tendsto line 32
  7. theorem OAI.JointDickman.auxiliaryCutoff_le_upper line 36
  8. theorem OAI.JointDickman.auxiliaryRatio_pos line 46
  9. theorem OAI.JointDickman.auxiliaryRatio_tendsto line 50
  10. theorem OAI.JointDickman.auxiliary_log_ratio line 66
  11. theorem OAI.JointDickman.auxiliary_primeNormalizer_tendsto line 74

    Source documentation

    The paper's Q_{z,B} ~ (4 R)^{-z} in normalized-limit form.

    theorem auxiliary_primeNormalizer_tendsto
    (hM : PublishedInputs.PrimeReciprocalMertensInput)
    {z : ℝ} (hz : 0 ≤ z) (hz1 : z ≤ 1) :
    Tendsto (fun B => primeNormalizer (auxiliaryPrimes B) z *
      auxiliaryRatio B ^ z) atTop (𝓝 ((4 : ℝ) ^ (-z))) := by
…

    Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.primeNormalizer, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.auxiliaryRatio