PrimeDivisors.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Prime-divisor budget in the collision argument

A distinct pair of integers at distance at most X contributes at most log X to the sum of log p over primes at which it collides. This is the elementary counting step behind the larger-sieve use in §§2–3.

theorem OAI.Ostmann.sum_log_prime_divisors_le line 23

Source documentation

Distinct prime divisors of a positive integer have total logarithmic weight at most the logarithm of that integer.

theorem sum_log_prime_divisors_le (P : Finset ℕ) {n : ℕ} (hn : 0 < n)
    (hprime : ∀ p ∈ P, p.Prime) (hdiv : ∀ p ∈ P, p ∣ n) :
    ∑ p ∈ P, Real.log (p : ℝ) ≤ Real.log (n : ℝ) := by
…

theorem OAI.Ostmann.sum_log_congruent_primes_le_of_sub_le line 38

Source documentation

The off-diagonal prime-collision budget, in the ordered-pair convention.

theorem sum_log_congruent_primes_le_of_sub_le (P : Finset ℕ) {x y X : ℕ}
    (hxy : x < y) (hdiff : y - x ≤ X) (hprime : ∀ p ∈ P, p.Prime) :
    ∑ p ∈ P.filter (fun p => x ≡ y [MOD p]), Real.log (p : ℝ) ≤
      Real.log (X : ℝ) := by
…

theorem OAI.Ostmann.sum_log_congruent_primes_le line 50

Source documentation

The collision budget for a pair in the initial interval [0,X].

theorem sum_log_congruent_primes_le (P : Finset ℕ) {x y X : ℕ}
    (hxy : x < y) (hy : y ≤ X) (hprime : ∀ p ∈ P, p.Prime) :
    ∑ p ∈ P.filter (fun p => x ≡ y [MOD p]), Real.log (p : ℝ) ≤
      Real.log (X : ℝ) :=
…