Rosser's linear sieve, combinatorial part ([I71, §2], k = 1)

• rosserSet lower y z: the supports D⁻ (lower = true) and D⁺ (lower = false) of Rosser's β = 2 sieve, defined recursively by D^± (y, z) = {1} ∪ ⋃_{p < z} p · D^∓ (y / p, p), where D⁺ only admits p³ < y.
• rosserSieve_le_siftIndicator_le: the sieve property ∑_{d ∈ D⁻, d ∣ m} μ(d) ≤ [(m, P(z)) = 1] ≤ ∑_{d ∈ D⁺, d ∣ m} μ(d), from Buchstab's identity.
• rosserMain lower y z = ∑_{d ∈ D^±} μ(d)/d and the depth-truncated deficits fail, with R(z) - rosserMain true y z = fail true r y z and rosserMain false y z - R(z) = fail false r y z for r > π(z) (fail_eq_of_card_lt); R(z) = 1 - ∑_{p < z} R(p)/p is R_eq.
• card_rosserSet, card_filter_rosserSet_succ: the counting recursions ([I71, Lemma 17]).

theorem IwaniecLinearSieve.lt_ceil_of_mem_primesLT {z : ℝ} {p : ℕ} (hp : p ∈ primesLT z) : p < ⌈z⌉₊

theorem IwaniecLinearSieve.prime_of_mem_primesLT {z : ℝ} {p : ℕ} (hp : p ∈ primesLT z) : Nat.Prime p

theorem IwaniecLinearSieve.lt_of_mem_primesLT {z : ℝ} {p : ℕ} (hp : p ∈ primesLT z) : ↑p < z

theorem IwaniecLinearSieve.primesLT_natCast_subset {z : ℝ} {p : ℕ} (hp : p ∈ primesLT z) : primesLT ↑p ⊆ primesLT z

theorem IwaniecLinearSieve.notMem_primesLT_self {p : ℕ} : p ∉ primesLT ↑p

theorem IwaniecLinearSieve.primesLT_natCast_ssubset {z : ℝ} {p : ℕ} (hp : p ∈ primesLT z) : primesLT ↑p ⊂ primesLT z

theorem IwaniecLinearSieve.filter_lt_primesLT {z : ℝ} {p : ℕ} (hp : p ∈ primesLT z) : {x ∈ primesLT z | x < p} = primesLT ↑p

For p < z prime, the primes below z that are smaller than p are the primes below p.

theorem IwaniecLinearSieve.primesLT_induction {P : ℝ → Prop} (h : ∀ (z : ℝ), (∀ p ∈ primesLT z, P ↑p) → P z) (z : ℝ) : P z

Strong induction on ⌈z⌉₊, descending from z to the primes below z.

theorem IwaniecLinearSieve.R_eq (z : ℝ) : R z = 1 - ∑ p ∈ primesLT z, R ↑p / ↑p

[I71, (2.11)] with k = 1: R(z) = 1 - ∑_{p < z} R(p) / p.

The sets D^±

noncomputable def IwaniecLinearSieve.rosserPrimes (lower : Bool) (y z : ℝ) : Finset ℕ

The primes p < z admitted at the top level of rosserSet lower y z: all of them for the lower-bound sieve, and those with p³ < y for the upper-bound sieve.

Equations

• IwaniecLinearSieve.rosserPrimes lower y z = {p ∈ IwaniecLinearSieve.primesLT z | lower = true ∨ ↑p ^ 3 < y}

@[irreducible]

noncomputable def IwaniecLinearSieve.rosserSet (lower : Bool) (y z : ℝ) : Finset ℕ

Rosser's sieve support (β = 2, [I71, §2]): rosserSet true y z is D⁻ and rosserSet false y z is D⁺. Equivalently d = p₁ ⋯ p_l with z > p₁ > ⋯ > p_l prime and p₁ ⋯ p_m p_m² < y for every m ≤ l which is even (for D⁻) or odd (for D⁺).

Equations

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

theorem IwaniecLinearSieve.mem_rosserPrimes {lower : Bool} {y z : ℝ} {p : ℕ} : p ∈ rosserPrimes lower y z ↔ p ∈ primesLT z ∧ (lower = true ∨ ↑p ^ 3 < y)

@[simp]

theorem IwaniecLinearSieve.rosserPrimes_true {y z : ℝ} : rosserPrimes true y z = primesLT z

theorem IwaniecLinearSieve.rosserPrimes_false {y z : ℝ} : rosserPrimes false y z = {p ∈ primesLT z | ↑p ^ 3 < y}

theorem IwaniecLinearSieve.rosserPrimes_subset {lower : Bool} {y z : ℝ} : rosserPrimes lower y z ⊆ primesLT z

theorem IwaniecLinearSieve.rosserSet_eq (lower : Bool) (y z : ℝ) : rosserSet lower y z = insert 1 ((rosserPrimes lower y z).biUnion fun (p : ℕ) => Finset.image (fun (x : ℕ) => p * x) (rosserSet (!lower) (y / ↑p) ↑p))

theorem IwaniecLinearSieve.one_mem_rosserSet {lower : Bool} {y z : ℝ} : 1 ∈ rosserSet lower y z

theorem IwaniecLinearSieve.mem_rosserSet {lower : Bool} {y z : ℝ} {d : ℕ} : d ∈ rosserSet lower y z ↔ d = 1 ∨ ∃ p ∈ rosserPrimes lower y z, ∃ e ∈ rosserSet (!lower) (y / ↑p) ↑p, d = p * e

theorem IwaniecLinearSieve.squarefree_and_primeFactors_subset {lower : Bool} {y z : ℝ} {d : ℕ} (hd : d ∈ rosserSet lower y z) : Squarefree d ∧ d.primeFactors ⊆ primesLT z

Elements of rosserSet lower y z are squarefree products of primes below z.

theorem IwaniecLinearSieve.squarefree_of_mem_rosserSet {lower : Bool} {y z : ℝ} {d : ℕ} (hd : d ∈ rosserSet lower y z) : Squarefree d

theorem IwaniecLinearSieve.primeFactors_subset_of_mem_rosserSet {lower : Bool} {y z : ℝ} {d : ℕ} (hd : d ∈ rosserSet lower y z) : d.primeFactors ⊆ primesLT z

theorem IwaniecLinearSieve.pos_of_mem_rosserSet {lower : Bool} {y z : ℝ} {d : ℕ} (hd : d ∈ rosserSet lower y z) : 0 < d

theorem IwaniecLinearSieve.dvd_primorialLT_of_mem_rosserSet {lower : Bool} {y z : ℝ} {d : ℕ} (hd : d ∈ rosserSet lower y z) : d ∣ primorialLT z

Elements of rosserSet are squarefree divisors of primorialLT z.

theorem IwaniecLinearSieve.lt_of_prime_dvd_of_mem_rosserSet {lower : Bool} {y z : ℝ} {d q : ℕ} (hq : Nat.Prime q) (hd : d ∈ rosserSet lower y z) (hqd : q ∣ d) : ↑q < z

theorem IwaniecLinearSieve.not_dvd_of_mem_rosserSet {lower : Bool} {y : ℝ} {p d : ℕ} (hp : Nat.Prime p) (hd : d ∈ rosserSet lower y ↑p) : ¬p ∣ d

theorem IwaniecLinearSieve.coprime_of_mem_rosserSet {lower : Bool} {y : ℝ} {p d : ℕ} (hp : Nat.Prime p) (hd : d ∈ rosserSet lower y ↑p) : p.Coprime d

theorem IwaniecLinearSieve.pairwiseDisjoint_rosserSet_image (lower : Bool) (y z : ℝ) : (↑(rosserPrimes lower y z)).PairwiseDisjoint fun (p : ℕ) => Finset.image (fun (x : ℕ) => p * x) (rosserSet (!lower) (y / ↑p) ↑p)

theorem IwaniecLinearSieve.one_notMem_biUnion_rosserSet (lower : Bool) (y z : ℝ) : 1 ∉ (rosserPrimes lower y z).biUnion fun (p : ℕ) => Finset.image (fun (x : ℕ) => p * x) (rosserSet (!lower) (y / ↑p) ↑p)

theorem IwaniecLinearSieve.sum_rosserSet {M : Type u_1} [AddCommMonoid M] (f : ℕ → M) (lower : Bool) (y z : ℝ) : ∑ d ∈ rosserSet lower y z, f d = f 1 + ∑ p ∈ rosserPrimes lower y z, ∑ d ∈ rosserSet (!lower) (y / ↑p) ↑p, f (p * d)

Sums over rosserSet unfold along the recursion.

theorem IwaniecLinearSieve.card_rosserSet (lower : Bool) (y z : ℝ) : (rosserSet lower y z).card = 1 + ∑ p ∈ rosserPrimes lower y z, (rosserSet (!lower) (y / ↑p) ↑p).card

The size of the sieve support satisfies the same recursion as the set.

theorem IwaniecLinearSieve.card_primeFactors_mul_of_mem_rosserSet {lower : Bool} {y : ℝ} {p d : ℕ} (hp : Nat.Prime p) (hd : d ∈ rosserSet lower y ↑p) : (p * d).primeFactors.card = d.primeFactors.card + 1

theorem IwaniecLinearSieve.card_filter_rosserSet_zero (lower : Bool) (y z : ℝ) : {d ∈ rosserSet lower y z | d.primeFactors.card ≤ 0}.card = 1

The elements of rosserSet with at most 0 prime factors.

theorem IwaniecLinearSieve.card_filter_rosserSet_succ (n : ℕ) (lower : Bool) (y z : ℝ) : {d ∈ rosserSet lower y z | d.primeFactors.card ≤ n + 1}.card = 1 + ∑ p ∈ rosserPrimes lower y z, {d ∈ rosserSet (!lower) (y / ↑p) ↑p | d.primeFactors.card ≤ n}.card

Depth-truncated counts ([I71, Lemma 17]): the elements of rosserSet with at most n + 1 prime factors.

Main terms

noncomputable def IwaniecLinearSieve.rosserMain (lower : Bool) (y z : ℝ) : ℝ

∑_{d ∈ D^±} μ(d) / d.

Equations

• IwaniecLinearSieve.rosserMain lower y z = ∑ d ∈ IwaniecLinearSieve.rosserSet lower y z, ↑(ArithmeticFunction.moebius d) / ↑d

theorem IwaniecLinearSieve.moebius_mul_of_mem_rosserSet {lower : Bool} {y : ℝ} {p d : ℕ} (hp : Nat.Prime p) (hd : d ∈ rosserSet lower y ↑p) : ArithmeticFunction.moebius (p * d) = -ArithmeticFunction.moebius d

theorem IwaniecLinearSieve.rosserMain_eq (lower : Bool) (y z : ℝ) : rosserMain lower y z = 1 - ∑ p ∈ rosserPrimes lower y z, rosserMain (!lower) (y / ↑p) ↑p / ↑p

The sieve property

noncomputable def IwaniecLinearSieve.siftIndicator (z : ℝ) (m : ℕ) : ℤ

1 if no prime p < z divides m, and 0 otherwise.

Equations

• IwaniecLinearSieve.siftIndicator z m = if ∀ p ∈ IwaniecLinearSieve.primesLT z, ¬p ∣ m then 1 else 0

theorem IwaniecLinearSieve.siftIndicator_nonneg (z : ℝ) (m : ℕ) : 0 ≤ siftIndicator z m

theorem IwaniecLinearSieve.siftIndicator_eq (z : ℝ) (m : ℕ) : siftIndicator z m = 1 - ∑ p ∈ primesLT z with p ∣ m, siftIndicator (↑p) m

Buchstab's identity for the indicator: [(m, P(z)) = 1] = 1 - ∑_{p < z, p ∣ m} [(m, P(p)) = 1], i.e. [I71, (2.3)] for a single integer.

theorem IwaniecLinearSieve.siftIndicator_of_dvd_primorialLT {z : ℝ} {m : ℕ} (hm : m ∣ primorialLT z) : siftIndicator z m = if m = 1 then 1 else 0

For m ∣ P(z), the indicator is [m = 1].

noncomputable def IwaniecLinearSieve.rosserSieve (lower : Bool) (y z : ℝ) (m : ℕ) : ℤ

∑_{d ∈ D^±, d ∣ m} μ(d).

Equations

• IwaniecLinearSieve.rosserSieve lower y z m = ∑ d ∈ IwaniecLinearSieve.rosserSet lower y z with d ∣ m, ArithmeticFunction.moebius d

theorem IwaniecLinearSieve.rosserSieve_eq (lower : Bool) (y z : ℝ) (m : ℕ) : rosserSieve lower y z m = 1 - ∑ p ∈ rosserPrimes lower y z with p ∣ m, rosserSieve (!lower) (y / ↑p) (↑p) m

theorem IwaniecLinearSieve.rosserSieve_le_siftIndicator_le (y z : ℝ) (m : ℕ) : rosserSieve true y z m ≤ siftIndicator z m ∧ siftIndicator z m ≤ rosserSieve false y z m

The sieve property of Rosser's weights, for every m: ∑_{d ∈ D⁻, d ∣ m} μ(d) ≤ [(m, P(z)) = 1] ≤ ∑_{d ∈ D⁺, d ∣ m} μ(d).

theorem IwaniecLinearSieve.sum_moebius_rosserSet_true_le (y z : ℝ) (m : ℕ) : ∑ d ∈ rosserSet true y z with d ∣ m, ArithmeticFunction.moebius d ≤ if ∀ p ∈ primesLT z, ¬p ∣ m then 1 else 0

Lower-bound sieve property: ∑_{d ∈ D⁻, d ∣ m} μ(d) ≤ [no prime p < z divides m].

theorem IwaniecLinearSieve.le_sum_moebius_rosserSet_false (y z : ℝ) (m : ℕ) : (if ∀ p ∈ primesLT z, ¬p ∣ m then 1 else 0) ≤ ∑ d ∈ rosserSet false y z with d ∣ m, ArithmeticFunction.moebius d

Upper-bound sieve property: [no prime p < z divides m] ≤ ∑_{d ∈ D⁺, d ∣ m} μ(d).

theorem IwaniecLinearSieve.rosserSieve_of_dvd_primorialLT {z : ℝ} (y : ℝ) {m : ℕ} (hm : m ∣ primorialLT z) : (∑ d ∈ rosserSet true y z with d ∣ m, ArithmeticFunction.moebius d ≤ if m = 1 then 1 else 0) ∧ (if m = 1 then 1 else 0) ≤ ∑ d ∈ rosserSet false y z with d ∣ m, ArithmeticFunction.moebius d

The sieve property for divisors of P(z): ∑_{d ∈ D⁻, d ∣ m} μ(d) ≤ [m = 1] ≤ ∑_{d ∈ D⁺, d ∣ m} μ(d).

The deficits R(z) - ∑_{D⁻} μ(d)/d and ∑_{D⁺} μ(d)/d - R(z)

noncomputable def IwaniecLinearSieve.fail : Bool → ℕ → ℝ → ℝ → ℝ

Depth-truncated deficits ([I71, (2.9), (2.10)] with k = 1): fail true r y z and fail false r y z are R(z) - ∑_{d ∈ D⁻} μ(d)/d and ∑_{d ∈ D⁺} μ(d)/d - R(z) computed to depth r.

Equations

• One or more equations did not get rendered due to their size.
• IwaniecLinearSieve.fail x✝² 0 x✝¹ x✝ = 0
• IwaniecLinearSieve.fail true r.succ x✝¹ x✝ = ∑ p ∈ IwaniecLinearSieve.primesLT x✝, IwaniecLinearSieve.fail false r (x✝¹ / ↑p) ↑p / ↑p

@[simp]

theorem IwaniecLinearSieve.fail_zero (lower : Bool) (y z : ℝ) : fail lower 0 y z = 0

theorem IwaniecLinearSieve.fail_true_succ (r : ℕ) (y z : ℝ) : fail true (r + 1) y z = ∑ p ∈ primesLT z, fail false r (y / ↑p) ↑p / ↑p

theorem IwaniecLinearSieve.fail_false_succ (r : ℕ) (y z : ℝ) : fail false (r + 1) y z = ∑ p ∈ rosserPrimes false y z, fail true r (y / ↑p) ↑p / ↑p + ∑ p ∈ primesLT z with ¬↑p ^ 3 < y, R ↑p / ↑p

theorem IwaniecLinearSieve.fail_nonneg (lower : Bool) (r : ℕ) (y z : ℝ) : 0 ≤ fail lower r y z

theorem IwaniecLinearSieve.fail_le_fail_succ (lower : Bool) (r : ℕ) (y z : ℝ) : fail lower r y z ≤ fail lower (r + 1) y z

theorem IwaniecLinearSieve.fail_mono (lower : Bool) (y z : ℝ) : Monotone fun (r : ℕ) => fail lower r y z

theorem IwaniecLinearSieve.fail_eq_of_card_lt {z : ℝ} {r : ℕ} (hr : (primesLT z).card < r) (y : ℝ) : fail true r y z = R z - rosserMain true y z ∧ fail false r y z = rosserMain false y z - R z

Once r exceeds the possible depth of the recursion, fail computes the deficits exactly ([I71, Lemma 2]).

theorem IwaniecLinearSieve.rosserMain_true_eq {z : ℝ} {r : ℕ} (hr : (primesLT z).card < r) (y : ℝ) : rosserMain true y z = R z - fail true r y z

∑_{d ∈ D⁻} μ(d)/d = R(z) - fail true r y z for r large.

theorem IwaniecLinearSieve.rosserMain_false_eq {z : ℝ} {r : ℕ} (hr : (primesLT z).card < r) (y : ℝ) : rosserMain false y z = R z + fail false r y z

∑_{d ∈ D⁺} μ(d)/d = R(z) + fail false r y z for r large.

theorem IwaniecLinearSieve.rosserMain_true_le_R (y z : ℝ) : rosserMain true y z ≤ R z

theorem IwaniecLinearSieve.R_le_rosserMain_false (y z : ℝ) : R z ≤ rosserMain false y z