PrimeNormalizer.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Normalization of the independent prime-product law

The logarithm of the all-absent probability is its linear prime sum up to a reciprocal-square error. Mertens' second theorem therefore determines the normalization for a moving lower and upper cutoff.

def OAI.JointDickman.primeNormalizer line 19

theorem OAI.JointDickman.prime_interval_mertens_error line 23

Source documentation

Both endpoint Mertens remainders control the prime-interval remainder.

theorem prime_interval_mertens_error
    (hM : PublishedInputs.PrimeReciprocalMertensInput) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ X Y : ℝ, 2 ≤ X → X ≤ Y →
      |(∑ p ∈ largePrimeSet Y X, 1 / (p : ℝ)) -
        (Real.log (Real.log Y) - Real.log (Real.log X))| ≤
        C / Real.log Y + C / Real.log X := by
…

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

theorem OAI.JointDickman.primeNormalizer_log_error line 45

Source documentation

Uniform logarithmic normalizer error, retaining both endpoint errors.

theorem primeNormalizer_log_error
    (hM : PublishedInputs.PrimeReciprocalMertensInput) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (N : ℕ) (Y z : ℝ), 2 ≤ N → (N : ℝ) ≤ Y →
      0 ≤ z → z ≤ 1 →
      |Real.log (primeNormalizer (largePrimeSet Y N) z) +
        z * Real.log (Real.log Y / Real.log N)| ≤
        2 * z ^ 2 / (N : ℝ) + z * (C / Real.log Y + C / Real.log N) := by
…

Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.primeNormalizer, OAI.JointDickman.largePrimeSet

theorem OAI.JointDickman.primeNormalizer_normalized_tendsto line 83

Source documentation

The all-absent product has the expected logarithmic normalization. Only Mertens' reciprocal-prime input is used.

theorem primeNormalizer_normalized_tendsto
    (hM : PublishedInputs.PrimeReciprocalMertensInput)
    (N : ℕ → ℕ) (Y : ℕ → ℝ) (hN : Tendsto N atTop atTop)
    (hY : Tendsto Y atTop atTop) (hNY : ∀ᶠ B in atTop, (N B : ℝ) ≤ Y B)
    {z : ℝ} (hz : 0 ≤ z) (hz1 : z ≤ 1) :
    Tendsto (fun B => primeNormalizer (largePrimeSet (Y B) (N B)) z *
      (Real.log (Y B) / Real.log (N B)) ^ z) atTop (𝓝 1) := by
…

Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.primeNormalizer, OAI.JointDickman.largePrimeSet