Prime-factor counts of the rough cofactor in Theorem 2

theorem NairTenenbaum.rough_bigOmega_lt_of_lt_pow {n k : ℕ} (hn : n ≠ 0) {z : ℝ} (hz : 1 ≤ z) (hrough : ∀ p ∈ n.primeFactors, z ≤ ↑p) (hsize : ↑n < z ^ k) : bigOmega n < k

theorem NairTenenbaum.log_le_bigOmega_mul_log {n : ℕ} (hn : n ≠ 0) {P : ℝ} (hP : 1 ≤ P) (hprimes : ∀ p ∈ n.primeFactors, ↑p ≤ P) : Real.log ↑n ≤ ↑(bigOmega n) * Real.log P

theorem NairTenenbaum.small_divisor_coprime_rough {d b : ℕ} (hd : 0 < d) (hb : b ≠ 0) {z : ℝ} (hdz : ↑d ≤ z) (hrough : ∀ p ∈ b.primeFactors, z < ↑p) : d.Coprime b

theorem NairTenenbaum.rough_cofactor_mul_divisor_le {a b d : ℕ} (hd : 0 < d) (hb : b ≠ 0) {z : ℝ} (hdz : ↑d ≤ z) (hrough : ∀ p ∈ b.primeFactors, z < ↑p) (hdab : d ∣ a * b) (ha : a ≠ 0) : d * b ≤ a * b

theorem NairTenenbaum.rough_cofactor_bigOmega_le {b k : ℕ} (hb : b ≠ 0) {A C y : ℝ} (hy : 1 ≤ y) (hC : 1 ≤ C) (hA : A < C ^ k) (hsize : ↑b ≤ A * y ^ k) (hrough : ∀ p ∈ b.primeFactors, C * y ≤ ↑p) : bigOmega b ≤ k - 1

theorem NairTenenbaum.rough_cofactor_bigOmega_le_of_window_divisor {n b d k : ℕ} (hb : b ≠ 0) (hk : 2 ≤ k) {A C y : ℝ} (hy : 1 ≤ y) (hC : 1 ≤ C) (hA : 2 * A < C ^ (k - 1)) (hsize : ↑n ≤ A * y ^ k) (hdiv : d * b ≤ n) (hd : y / 2 < ↑d) (hrough : ∀ p ∈ b.primeFactors, C * y ≤ ↑p) : bigOmega b ≤ k - 2