Documentation

PrimeNumberTheoremAnd.BrunTitchmarsh

def BrunTitchmarsh.primeInterSieve (x y z : ℝ) (hz : 1 ≤ z) :

Equations

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

Instances For

def BrunTitchmarsh.primesBetween (a b : ℝ) :

Equations

BrunTitchmarsh.primesBetween a b = (Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊b⌋₊)).card

Instances For

theorem BrunTitchmarsh.siftedSum_eq_card (x y z : ℝ) (hz : 1 ≤ z) :

SelbergSieve.siftedSum = ↑{d ∈ Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊ | ∀ (p : ℕ), Nat.Prime p → ↑p ≤ z → ¬p ∣ d}.card

theorem BrunTitchmarsh.primesBetween_subset (x y z : ℝ) :

Finset.filter Nat.Prime (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) ⊆ {d ∈ Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊ | ∀ (p : ℕ), Nat.Prime p → ↑p ≤ z → ¬p ∣ d} ∪ Finset.Icc 1 ⌊z⌋₊

theorem BrunTitchmarsh.primesBetween_le_siftedSum_add (x y z : ℝ) (hz : 1 ≤ z) :

↑(primesBetween x (x + y)) ≤ SelbergSieve.siftedSum + z

theorem BrunTitchmarsh.Ioc_filter_dvd_eq (d a b : ℕ) (hd : d ≠ 0) :

{x ∈ Finset.Ioc a b | d ∣ x} = Finset.image (fun (x : ℕ) => x * d) (Finset.Ioc (a / d) (b / d))

theorem BrunTitchmarsh.card_Ioc_filter_dvd (d a b : ℕ) (hd : d ≠ 0) :

{x ∈ Finset.Ioc a b | d ∣ x}.card = b / d - a / d

theorem BrunTitchmarsh.multSum_eq (x y z : ℝ) (hx : 0 < x) (hz : 1 ≤ z) (d : ℕ) (hd : d ≠ 0) :

SelbergSieve.multSum d = ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d)

theorem BrunTitchmarsh.rem_eq (x y z : ℝ) (hx : 0 < x) (hz : 1 ≤ z) (d : ℕ) (hd : d ≠ 0) :

SelbergSieve.rem d = ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y

theorem BrunTitchmarsh.Nat.ceil_le_self_add_one (x : ℝ) (hx : 0 ≤ x) :

↑⌈x⌉₊ ≤ x + 1

theorem BrunTitchmarsh.floor_approx (x : ℝ) (hx : 0 ≤ x) :

∃ (C : ℝ), |C| ≤ 1 ∧ ↑⌊x⌋₊ = x + C

theorem BrunTitchmarsh.ceil_approx (x : ℝ) (hx : 0 ≤ x) :

∃ (C : ℝ), |C| ≤ 1 ∧ ↑⌈x⌉₊ = x + C

theorem BrunTitchmarsh.nat_div_approx (a b : ℕ) :

∃ (C : ℝ), |C| ≤ 1 ∧ ↑(a / b) = ↑a / ↑b + C

theorem BrunTitchmarsh.floor_div_approx (x : ℝ) (hx : 0 ≤ x) (d : ℕ) :

∃ (C : ℝ), |C| ≤ 2 ∧ ↑(⌊x⌋₊ / d) = x / ↑d + C

theorem BrunTitchmarsh.abs_rem_le (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 1 ≤ z) {d : ℕ} (hd : d ≠ 0) :

|SelbergSieve.rem d| ≤ 5

theorem BrunTitchmarsh.boudingSum_ge (x y z : ℝ) (hz : 1 ≤ z) :

(primeInterSieve x y z hz).selbergBoundingSum ≥ Real.log z / 2

theorem BrunTitchmarsh.primeSieve_rem_sum_le (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 1 ≤ z) :

(∑ d ∈ BoundingSieve.prodPrimes.divisors, if ↑d ≤ z then 3 ^ ArithmeticFunction.cardDistinctFactors d * |SelbergSieve.rem d| else 0) ≤ 5 * z * (1 + Real.log z) ^ 3

theorem BrunTitchmarsh.siftedSum_le (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 1 < z) :

SelbergSieve.siftedSum ≤ 2 * y / Real.log z + 5 * z * (1 + Real.log z) ^ 3

theorem BrunTitchmarsh.primesBetween_le (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 1 < z) :

↑(primesBetween x (x + y)) ≤ 2 * y / Real.log z + 6 * z * (1 + Real.log z) ^ 3

theorem BrunTitchmarsh.primesBetween_one (n : ℕ) :

primesBetween 1 ↑n = (Finset.filter Nat.Prime (Finset.range (n + 1))).card

theorem BrunTitchmarsh.primesBetween_mono_right (a b c : ℝ) (hbc : b ≤ c) :

primesBetween a b ≤ primesBetween a c

theorem BrunTitchmarsh.tmp (N : ℕ) :

↑(Finset.filter Nat.Prime (Finset.range N)).card ≤ 4 * (↑N / Real.log ↑N) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * Real.log ↑N) ^ 3)

theorem BrunTitchmarsh.rpow_mul_rpow_log_isBigO_id_div_log (k : ℝ) {r : ℝ} (hr : r < 1) :

(fun (x : ℝ) => x ^ r * Real.log x ^ k) =O[Filter.atTop ] fun (x : ℝ) => x / Real.log x

theorem BrunTitchmarsh.err_isBigO :

(fun (x : ℝ) => x ^ (1 / 2) * (1 + 1 / 2 * Real.log x) ^ 3) =O[Filter.atTop ] fun (x : ℝ) => x / Real.log x

theorem BrunTitchmarsh.card_range_filter_prime_isBigO :

(fun (N : ℕ) => ↑(Finset.filter Nat.Prime (Finset.range N)).card) =O[Filter.atTop ] fun (N : ℕ) => ↑N / Real.log ↑N

theorem BrunTitchmarsh.prime_or_pow (N n : ℕ) (hnN : n < N) (hnprime : IsPrimePow n) :

Nat.Prime n ∨ ∃ (m : ℕ), ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k

theorem BrunTitchmarsh.Nat.log_eq_floor_logb (b n : ℕ) (hb : 1 < b) :

Nat.log b n = ⌊Real.logb ↑b ↑n⌋₊

theorem BrunTitchmarsh.range_filter_isPrimePow_subset_union (N : ℕ) :

Finset.filter IsPrimePow (Finset.range N) ⊆ Finset.filter Nat.Prime (Finset.range N) ∪ Finset.image (fun (p : ℕ × ℕ) => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))

theorem BrunTitchmarsh.IsBigO.nat_Top_of_atTop (f g : ℕ → ℝ) (h : f =O[Filter.atTop ] g) (h0 : ∀ (n : ℕ), g n = 0 → f n = 0) :

theorem BrunTitchmarsh.pows_small_primes_le (N : ℕ) :

↑(Finset.image (fun (p : ℕ × ℕ) => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card ≤ ↑N ^ (1 / 2) * (1 + Real.log ↑N / Real.log 2)

theorem BrunTitchmarsh.one_add_log_div_log_two_isBigO :

(fun (N : ℝ) => 1 + Real.log N / Real.log 2) =O[Filter.atTop ] fun (N : ℝ) => Real.log N

theorem BrunTitchmarsh.pow_half_mul_one_add_log_div_isBigO :

(fun (N : ℝ) => N ^ (1 / 2) * (1 + Real.log N / Real.log 2)) =O[Filter.atTop ] fun (N : ℝ) => N / Real.log N

theorem BrunTitchmarsh.card_pows_aux :

(fun (N : ℕ) => ↑(Finset.image (fun (p : ℕ × ℕ) => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card) =O[Filter.atTop ] fun (N : ℕ) => ↑N / Real.log ↑N

theorem BrunTitchmarsh.card_isPrimePow_isBigO :

(fun (N : ℕ) => ↑(Finset.filter IsPrimePow (Finset.range N)).card) =O[Filter.atTop ] fun (N : ℕ) => ↑N / Real.log ↑N

theorem BrunTitchmarsh.card_range_filter_isPrimePow_le :

∃ (C : ℝ), ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / Real.log ↑N)