Actual rough integers and the finite Buchstab identity

The carrier consists of positive natural numbers bounded by a real number. The cutoff excludes primes strictly below z; in particular the unit is retained and a prime equal to the cutoff is not excluded.

def LiLiuPrereqBuchstab.Rough (z : ℝ) (n : ℕ) : Prop

Equations

• LiLiuPrereqBuchstab.Rough z n = ∀ (p : ℕ), Nat.Prime p → p ∣ n → z ≤ ↑p

noncomputable def LiLiuPrereqBuchstab.roughNumbers (x z : ℝ) : Finset ℕ

Equations

• LiLiuPrereqBuchstab.roughNumbers x z = {n ∈ Finset.range (⌊x⌋₊ + 1) | 0 < n ∧ ↑n ≤ x ∧ LiLiuPrereqBuchstab.Rough z n}

noncomputable def LiLiuPrereqBuchstab.roughCount (x z : ℝ) : ℕ

Equations

• LiLiuPrereqBuchstab.roughCount x z = (LiLiuPrereqBuchstab.roughNumbers x z).card

@[simp]

theorem LiLiuPrereqBuchstab.mem_roughNumbers {x z : ℝ} {n : ℕ} : n ∈ roughNumbers x z ↔ 0 < n ∧ ↑n ≤ x ∧ Rough z n

theorem LiLiuPrereqBuchstab.rough_iff_no_small_prime {z : ℝ} {n : ℕ} : Rough z n ↔ ∀ (p : ℕ), Nat.Prime p → ↑p < z → ¬p ∣ n

theorem LiLiuPrereqBuchstab.rough_one (z : ℝ) : Rough z 1

@[simp]

theorem LiLiuPrereqBuchstab.one_mem_roughNumbers {x z : ℝ} : 1 ∈ roughNumbers x z ↔ 1 ≤ x

theorem LiLiuPrereqBuchstab.rough_mono {y z : ℝ} (hyz : y ≤ z) {n : ℕ} (hn : Rough z n) : Rough y n

theorem LiLiuPrereqBuchstab.roughNumbers_mono {x y z : ℝ} (hyz : y ≤ z) : roughNumbers x z ⊆ roughNumbers x y

theorem LiLiuPrereqBuchstab.rough_iff_minFac {z : ℝ} {n : ℕ} (hn : n ≠ 1) : Rough z n ↔ z ≤ ↑n.minFac

theorem LiLiuPrereqBuchstab.rough_mul_prime {p m : ℕ} (hp : Nat.Prime p) (hm : Rough (↑p) m) : Rough (↑p) (p * m)

theorem LiLiuPrereqBuchstab.minFac_mul_of_rough {p m : ℕ} (hp : Nat.Prime p) (hm : Rough (↑p) m) : (p * m).minFac = p

theorem LiLiuPrereqBuchstab.rough_div_minFac (n : ℕ) : Rough (↑n.minFac) (n / n.minFac)

theorem LiLiuPrereqBuchstab.rough_of_dvd {z : ℝ} {m n : ℕ} (hmn : m ∣ n) (hn : Rough z n) : Rough z m

noncomputable def LiLiuPrereqBuchstab.sievingPrimes (x y z : ℝ) : Finset ℕ

Only primes at most x can occur as least factors of the removed integers.

Equations

• LiLiuPrereqBuchstab.sievingPrimes x y z = {p ∈ Finset.range (⌊x⌋₊ + 1) | Nat.Prime p ∧ ↑p ≤ x ∧ y ≤ ↑p ∧ ↑p < z}

@[simp]

theorem LiLiuPrereqBuchstab.mem_sievingPrimes {x y z : ℝ} {p : ℕ} : p ∈ sievingPrimes x y z ↔ Nat.Prime p ∧ ↑p ≤ x ∧ y ≤ ↑p ∧ ↑p < z

theorem LiLiuPrereqBuchstab.removed_ne_one {x y z : ℝ} {n : ℕ} (hn : n ∈ roughNumbers x y \ roughNumbers x z) : n ≠ 1

theorem LiLiuPrereqBuchstab.minFac_mem_sievingPrimes {x y z : ℝ} {n : ℕ} (hn : n ∈ roughNumbers x y \ roughNumbers x z) : n.minFac ∈ sievingPrimes x y z

theorem LiLiuPrereqBuchstab.card_leastFactor_fiber {x y z : ℝ} {p : ℕ} (hp : Nat.Prime p) (hyp : y ≤ ↑p) (hpz : ↑p < z) : {n ∈ roughNumbers x y \ roughNumbers x z | n.minFac = p}.card = roughCount (x / ↑p) ↑p

Multiplication by the least prime factor is an actual finite bijection. The cofactor may still be divisible by p, as required at prime squares.

theorem LiLiuPrereqBuchstab.roughCount_buchstab {x y z : ℝ} (hyz : y ≤ z) : roughCount x y = roughCount x z + ∑ p ∈ sievingPrimes x y z, roughCount (x / ↑p) ↑p

Exact Buchstab decomposition of the actual positive-integer rough count, with real upper bounds and the strict small-prime cutoff.