Documentation

LeanPool.SelbergSieve4.Applications.BrunTitchmarsh

LeanPool.SelbergSieve4.Applications.BrunTitchmarsh #

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

Sieve that removes primes at most z from the interval [x, x + y].

Equations

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

Instances For

noncomputable def BrunTitchmarsh.primesBetween (a b : ℝ) :

Number of primes in the real interval [a, b].

Equations

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

Instances For

theorem BrunTitchmarsh.primesBetween_eq_ncard {a b : ℝ} (hb : 0 ≤ b) :

primesBetween a b = {p : ℕ | a ≤ ↑p ∧ ↑p ≤ b ∧ Nat.Prime p}.ncard

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

(primeInterSieve x y z hz).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)) ≤ (primeInterSieve x y z hz).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 : ℝ) (hz : 1 ≤ z) (hx : 0 < x) (d : ℕ) (hd : d ≠ 0) :

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

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

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

theorem BrunTitchmarsh.natCeil_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 : ℝ) (hz : 1 ≤ z) (hx : 0 < x) (hy : 0 < y) {d : ℕ} (hd : d ≠ 0) :

|(primeInterSieve x y z hz).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 : ℝ) (hz : 1 ≤ z) (hx : 0 < x) (hy : 0 < y) :

(∑ d ∈ (primeInterSieve x y z hz).prodPrimes.divisors, if ↑d ≤ z then 3 ^ ArithmeticFunction.cardDistinctFactors d * |(primeInterSieve x y z hz).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) :

(primeInterSieve x y z ⋯).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