LeanPool.SelbergSieve4.MainResults

theorem fundamental_theorem_simple (s : SelbergSieve) : s.siftedSum ≤ s.totalMass / s.selbergBoundingSum + ∑ d ∈ s.prodPrimes.divisors, if ↑d ≤ s.level then 3 ^ ArithmeticFunction.cardDistinctFactors d * |s.rem d| else 0

theorem primeCounting_isBigO_atTop : (fun (N : ℕ) => ↑N.primeCounting) =O[Filter.atTop] fun (N : ℕ) => ↑N / Real.log ↑N

theorem primeCounting_le_mul : ∃ (N : ℕ) (C : ℝ), ∀ n ≥ N, ↑n.primeCounting ≤ C * ↑n / Real.log ↑n

theorem primesBetween_le (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 1 < z) : ↑{p : ℕ | x ≤ ↑p ∧ ↑p ≤ x + y ∧ Nat.Prime p}.ncard ≤ 2 * y / Real.log z + 6 * z * (1 + Real.log z) ^ 3