Smooth and rough parts at a real cutoff

noncomputable def NairTenenbaum.smoothPart (n : ℕ+) (z : ℝ) : ℕ+

The factor supported on primes up to the smoothness cutoff.

Equations

• NairTenenbaum.smoothPart n z = NairTenenbaum.primeSelect (fun (x : Fin 1) => n) (Finset.range (⌊z⌋₊ + 1)) 0

noncomputable def NairTenenbaum.roughPart (n : ℕ+) (z : ℝ) : ℕ+

The complementary factor supported on primes above the smoothness cutoff.

Equations

• NairTenenbaum.roughPart n z = NairTenenbaum.primeReject (fun (x : Fin 1) => n) (Finset.range (⌊z⌋₊ + 1)) 0

theorem NairTenenbaum.smoothPart_mul_roughPart (n : ℕ+) (z : ℝ) : smoothPart n z * roughPart n z = n

theorem NairTenenbaum.cutoff_lt_of_mem_roughPart (n : ℕ+) (z : ℝ) {p : ℕ} (hp : p ∈ (↑(roughPart n z)).primeFactors) : z < ↑p

theorem NairTenenbaum.log_roughPart (n : ℕ+) (z : ℝ) : Real.log ↑↑(roughPart n z) = Real.log ↑↑n - Real.log ↑↑(smoothPart n z)