LeanPool.SelbergSieve4.Applications.PrimeCountingUpperBound

theorem PrimeUpperBound.prodDistinctPrimes_squarefree (s : Finset ℕ) (h : ∀ p ∈ s, Nat.Prime p) : Squarefree (∏ p ∈ s, p)

theorem PrimeUpperBound.primorial_squarefree (n : ℕ) : Squarefree (primorial n)

theorem PrimeUpperBound.zeta_pos_of_prime (p : ℕ) : Nat.Prime p → 0 < ↑ArithmeticFunction.zeta p

theorem PrimeUpperBound.zeta_lt_self_of_prime (p : ℕ) : Nat.Prime p → ↑ArithmeticFunction.zeta p < ↑p

noncomputable def PrimeUpperBound.primeSieve (N : ℕ) (y : ℝ) (hy : 1 ≤ y) : SelbergSieve

Selberg sieve specialized to primes at most the real level y.

Equations

• One or more equations did not get rendered due to their size.

theorem PrimeUpperBound.prime_dvd_primorial_iff (n p : ℕ) (hp : Nat.Prime p) : p ∣ primorial n ↔ p ≤ n

theorem PrimeUpperBound.siftedSum_eq (s : SelbergSieve) (hw : ∀ i ∈ s.support, s.weights i = 1) (z : ℝ) (hz : 1 ≤ z) (hP : s.prodPrimes = primorial ⌊z⌋₊) : s.siftedSum = ↑{d ∈ s.support | ∀ (p : ℕ), Nat.Prime p → ↑p ≤ z → ¬p ∣ d}.card

theorem PrimeUpperBound.primeSieve_siftedSum_eq (N : ℕ) (y : ℝ) (hy : 1 ≤ y) : (primeSieve N y hy).siftedSum = ↑{d ∈ Finset.range (N + 1) | ∀ (p : ℕ), Nat.Prime p → ↑p ≤ y → ¬p ∣ d}.card

theorem PrimeUpperBound.prime_subset (N : ℕ) (y : ℝ) : Finset.filter Nat.Prime (Finset.range (N + 1)) ⊆ {d ∈ Finset.range (N + 1) | ∀ (p : ℕ), Nat.Prime p → ↑p ≤ y → ¬p ∣ d} ∪ Finset.Icc 1 ⌊y⌋₊

theorem PrimeUpperBound.pi_le_siftedSum (N : ℕ) (y : ℝ) (hy : 1 ≤ y) : ↑N.primeCounting ≤ (primeSieve N y hy).siftedSum + y

def PrimeUpperBound.CompletelyMultiplicative (f : ArithmeticFunction ℝ) : Prop

Predicate asserting that an arithmetic function is completely multiplicative.

Equations

• PrimeUpperBound.CompletelyMultiplicative f = (f 1 = 1 ∧ ∀ (a b : ℕ), f (a * b) = f a * f b)

theorem PrimeUpperBound.CompletelyMultiplicative.zeta : CompletelyMultiplicative ↑ArithmeticFunction.zeta

theorem PrimeUpperBound.CompletelyMultiplicative.id : CompletelyMultiplicative ↑ArithmeticFunction.id

theorem PrimeUpperBound.CompletelyMultiplicative.pmul (f g : ArithmeticFunction ℝ) (hf : CompletelyMultiplicative f) (hg : CompletelyMultiplicative g) : CompletelyMultiplicative (f.pmul g)

theorem PrimeUpperBound.CompletelyMultiplicative.pdiv {f g : ArithmeticFunction ℝ} (hf : CompletelyMultiplicative f) (hg : CompletelyMultiplicative g) : CompletelyMultiplicative (f.pdiv g)

theorem PrimeUpperBound.CompletelyMultiplicative.isMultiplicative {f : ArithmeticFunction ℝ} (hf : CompletelyMultiplicative f) : f.IsMultiplicative

theorem PrimeUpperBound.CompletelyMultiplicative.apply_pow (f : ArithmeticFunction ℝ) (hf : CompletelyMultiplicative f) (a n : ℕ) : f (a ^ n) = f a ^ n

theorem PrimeUpperBound.prod_factors_one_div_compMult_ge (M : ℕ) (f : ArithmeticFunction ℝ) (hf : CompletelyMultiplicative f) (hf_nonneg : ∀ (n : ℕ), 0 ≤ f n) (d : ℕ) (hd : Squarefree d) (hf_size : ∀ (n : ℕ), Nat.Prime n → n ∣ d → f n < 1) : f d * ∏ p ∈ d.primeFactors, 1 / (1 - f p) ≥ ∏ p ∈ d.primeFactors, ∑ n ∈ Finset.Icc 1 M, f (p ^ n)

theorem PrimeUpperBound.prod_factors_sum_pow_compMult (M : ℕ) (hM : M ≠ 0) (f : ArithmeticFunction ℝ) (hf : CompletelyMultiplicative f) (d : ℕ) (hd : Squarefree d) : ∏ p ∈ d.primeFactors, ∑ n ∈ Finset.Icc 1 M, f (p ^ n) = ∑ m ∈ (d ^ M).divisors with d ∣ m, f m

theorem PrimeUpperBound.lem0 (P : ℕ) {s : Finset ℕ} (h : ∀ p ∈ s, p ∣ P) (h' : ∀ p ∈ s, Nat.Prime p) : ∏ p ∈ s, p ∣ P

theorem PrimeUpperBound.sqrt_le_self (x : ℝ) (hx : 1 ≤ x) : √x ≤ x

theorem PrimeUpperBound.nat_squarefree_dvd_pow (a b N : ℕ) (ha : Squarefree a) (hab : a ∣ b ^ N) : a ∣ b

theorem PrimeUpperBound.selbergBoundingSum_ge_sum_div (s : SelbergSieve) (hP : ∀ (p : ℕ), Nat.Prime p → ↑p ≤ s.level → p ∣ s.prodPrimes) (hnu : CompletelyMultiplicative s.nu) (hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n) (hnu_lt : ∀ (p : ℕ), Nat.Prime p → p ∣ s.prodPrimes → s.nu p < 1) : s.selbergBoundingSum ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, s.nu m

theorem PrimeUpperBound.boundingSum_ge_sum (s : SelbergSieve) (hnu : s.nu = (↑ArithmeticFunction.zeta).pdiv ↑ArithmeticFunction.id) (hP : ∀ (p : ℕ), Nat.Prime p → ↑p ≤ s.level → p ∣ s.prodPrimes) : s.selbergBoundingSum ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m

theorem PrimeUpperBound.boundingSum_ge_log (s : SelbergSieve) (hnu : s.nu = (↑ArithmeticFunction.zeta).pdiv ↑ArithmeticFunction.id) (hP : ∀ (p : ℕ), Nat.Prime p → ↑p ≤ s.level → p ∣ s.prodPrimes) : s.selbergBoundingSum ≥ Real.log s.level / 2

theorem PrimeUpperBound.primeSieve_boundingSum_ge (N : ℕ) (y : ℝ) (hy : 1 ≤ y) : (primeSieve N y hy).selbergBoundingSum ≥ Real.log y / 2

theorem PrimeUpperBound.card_range_filter_dvd (N d : ℕ) (hd : d ≠ 0) : {x ∈ Finset.range N | d ∣ x}.card = ⌈↑N / ↑d⌉₊

theorem PrimeUpperBound.primeSieve_multSum_eq (N : ℕ) (y : ℝ) (hy : 1 ≤ y) (d : ℕ) (hd : d ≠ 0) : (primeSieve N y hy).multSum d = ↑⌈↑(N + 1) / ↑d⌉₊

theorem PrimeUpperBound.primeSieve_rem_eq (N : ℕ) (y : ℝ) (hy : 1 ≤ y) (d : ℕ) (hd : d ≠ 0) : (primeSieve N y hy).rem d = ↑⌈↑(N + 1) / ↑d⌉₊ - ↑N / ↑d

theorem PrimeUpperBound.primeSieve_abs_rem_eq (N : ℕ) (y : ℝ) (hy : 1 ≤ y) (d : ℕ) (hd : d ≠ 0) : |(primeSieve N y hy).rem d| ≤ 2

theorem PrimeUpperBound.rem_sum_le_of_const (s : SelbergSieve) (C : ℝ) (hrem : ∀ d > 0, |s.rem d| ≤ C) : (∑ d ∈ s.prodPrimes.divisors, if ↑d ≤ s.level then 3 ^ ArithmeticFunction.cardDistinctFactors d * |s.rem d| else 0) ≤ C * s.level * (1 + Real.log s.level) ^ 3

theorem PrimeUpperBound.primeSieve_rem_sum_le (N : ℕ) (y : ℝ) (hy : 1 ≤ y) : (∑ d ∈ (primeSieve N y hy).prodPrimes.divisors, if ↑d ≤ y then 3 ^ ArithmeticFunction.cardDistinctFactors d * |(primeSieve N y hy).rem d| else 0) ≤ ↑2 * y * (1 + Real.log y) ^ 3

theorem PrimeUpperBound.pi_le_of_y (N : ℕ) (y : ℝ) (hy_lt : 1 < y) : ↑N.primeCounting ≤ ↑2 * ↑N / Real.log y + ↑3 * y * (1 + Real.log y) ^ 3

theorem PrimeUpperBound.primeCounting_zero : Nat.primeCounting 0 = 0

theorem PrimeUpperBound.primeCounting_one : Nat.primeCounting 1 = 0

theorem PrimeUpperBound.loglog_nonneg (x : ℝ) (hx : 3 ≤ x) : 0 ≤ Real.log (Real.log x)

theorem PrimeUpperBound.loglog_bigO_log : (fun (N : ℕ) => Real.log (Real.log ↑N)) =O[Filter.atTop] fun (N : ℕ) => Real.log ↑N

theorem PrimeUpperBound.pi_le_id_div_log_of_eps (N : ℕ) (ε : ℝ) (_hε_pos : ε > 0) (hε : ε < 1) : ↑N.primeCounting ≤ ↑2 / (↑1 - ε) * ↑N / Real.log ↑N + ↑3 * ↑N ^ (1 - ε) * (1 + (1 - ε) * Real.log ↑N) ^ 3

theorem PrimeUpperBound.pi_le_id_div_log (N : ℕ) : ↑N.primeCounting ≤ 4 * ↑N / Real.log ↑N + 3 * ↑N ^ (1 / 2) * (1 + 1 / 2 * Real.log ↑N) ^ 3

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

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