PrimeProductSmallTail.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Small prime products and absent large primes

A small product must omit every prime above its size. Independence turns this observation into an exact all-absent product bound.

theorem OAI.JointDickman.bernoulliSubsetMass_subset_sum line 18
theorem OAI.JointDickman.primeProduct_small_bound line 49

theorem OAI.JointDickman.primeProduct_small_log_tail line 88

Source documentation

The manuscript's uniform small-log-product tail, including the empty product.

theorem primeProduct_small_log_tail
    (hM : PublishedInputs.PrimeReciprocalMertensInput) {z : ℝ}
    (hz : 0 ≤ z) (hz1 : z ≤ 1) :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ B : ℕ in atTop, ∀ δ : ℝ, 0 ≤ δ → δ ≤ 1 →
      (∑ S ∈ (auxiliaryPrimes B).powerset,
        if Real.log (∏ p ∈ S, p : ℕ) / B ≤ δ then
          bernoulliSubsetMass (auxiliaryPrimes B) (fun p => z / p) S else 0) ≤
        C * (δ + 1 / auxiliaryRatio B) ^ z := by
…

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